SIGMA

# DEPENDENT SUM

-type is a total space of fibration. Element of total space is formed as a pair of basepoint and fibration.
Categorically, is a dependent product type, the generalization of products or disjoint union of family of sets.

## Definition

(Dependent Sum). The dependent sum along the morphism in category is the left adjoint of the base change functor.

## Constructors

def pair (A: U) (B: A → U) (a: A) (b: B a) : Sigma A B := (a, b)

## Eliminators

pr1 (A: U) (B: A -> U) (x: Sigma A B): A = x.1 pr2 (A: U) (B: A -> U) (x: Sigma A B): B (pr1 A B x) = x.2 

If you want to access deep sigma a series of accessors should be applied followed by .

## Induction Principle

Dependent Elimination Principle states that if predicate holds for two projections then predicate holds for total space.

sigInd (A: U) (B: A -> U) (C: Sigma A B -> U) (g: (a: A) (b: B a) -> C (a, b)) (p: Sigma A B): C p = g p.1 p.2

## Computation and Uniquness

Beta1 (A: U) (B: A -> U) (a:A) (b: B a) : Equ A a (pr1 A B (a,b)) = refl A a Beta2 (A: U) (B: A -> U) (a: A) (b: B a) : Equ (B a) b (pr2 A B (a,b)) = reflect (B a)
Eta12 (A: U) (B: A -> U) (p: Sigma A B) : Equ (Sigma A B) p (pr1 A B p,pr2 A B p) = refl (Sigma A B) p

# Theorems

(Axiom of Choice). If for all there is such that , then there is a function such that for all there is a witness of .

ac (A B: U) (R: A -> B -> U): (p: (x:A)->(y:B)*(R x y)) -> (f:A->B)*((x:A)->R(x)(f x)) = \(g: (x:A)->(y:B)*(R x y)) -> (\(i:A)->(g i).1,\(j:A)->(g j).2) 

(Total). If fiber over base implies another fiber over the same base then we can construct total space of section over that base with another fiber.

total (A:U) (B C: A -> U) (f: (x:A) -> B x -> C x) (w: Sigma A B) : Sigma A C = (w.1,f (w.1) (w.2)) 

(Path Between Sigmas). Path between two sigmas could be decomposed to sigma of two paths and .

pathSig (A:U) (B : A -> U) (t u : Sigma A B) : Path U (Path (Sigma A B) t u) ( (p : Path A t.1 u.1) * PathP (<i> B (p @ i)) t.2 u.2) 

(Propositions). If codomain of dependent the function is a mere proposition and for two sigmas there is a path then the path between second components is a mere proposition too. Same if codomain is set.

corSigProp (A:U) (B:A-> U) (pB: (x:A) -> isProp (B x)) (t u: Sigma A B) (p:Path A t.1 u.1): isProp (PathP (<i>B ([email protected])) t.2 u.2) corSigSet (A:U) (B:A-> U) (sB: (x:A) -> isSet (B x)) (t u: Sigma A B) (p: Path A t.1 u.1): isProp (PathP (<i>B ([email protected])) t.2 u.2) 

(Contractability). If first and second component of sigma are contractible then the total space of sigma is contractible.

sigmaIsContr (A: U) (B: A -> U) (u: isContr A) (q: (x: A) -> isContr (B x)) : isContr (Sigma A B)