# 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)