sigma

Sigma package contains basic theorems about sigma types. Sigma type is built in MLTT core.

Sigma (A : U) (B : A -> U) : U = (x : A) * B x

Sigma is a dependent product type, the generalization of products.

Sigma type is a total space of fibration. Element of total space is formed as a pair of basepoint and fibration.

Definition

Definition (Dependent Sum). The dependent sum along the morphism $f: A \rightarrow B$ in category $C$ is the left adjoint $\Sigma_f : C_{/A} \rightarrow C_{/B}$ of the base change functor.

Introduction

dpair (A: U) (B: A -> U) (a: A) (b: B a): Sigma A B = (a,b)

Elimination

Pair accessors

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 .2 accessors should be applied followed by .1.

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

Beta

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)

Eta

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

Theorem (Axiom of Choice). If for all $x : A$ there is $y : B$ such that $R(x,y)$, then there is a function $f : A \rightarrow B$ such that for all $x : A$ there is a witness of $R(x,f(x))$.

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)

Theorem (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))

Theorem (Path Between Sigmas). Path between two sigmas $t,u: \Sigma(A,B)$ could be decomposed to sigma of two paths $p:t_1=_{A}u_1)$ and $(t_2=_{B([email protected])}u_2)$.

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)

Theorem (Propositions). If codomain $B: A \rightarrow U$ of dependent the function $f: (x:A) \rightarrow B(x)$ is a mere proposition and for two sigmas $t,u: \Sigma(A,B)$ there is a path $Path_A(t_1,u_1)$ then the path between second components $Path_{B([email protected])}(t_2,u_2)$ 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)

Theorem (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)