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

All the constructions on $\Sigma$-types arise as straightforward generalizations of the ones for product types. the type of the second component of a pair to vary depending on the choice of the first component. This is called a dependent pair type, because in set theory it corresponds to an indexed sum (in the sense of coproduct or disjoint union) over a given type.

Intro

Pair

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

Pair constructor is also built in core as $(a,b)$. Here is shown how we can define the proper signature of intro constructor.

Eliminators

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

Induction

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

Recursor is the special case of induction when the family $C$ is constant.

Theorems

pathSig

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)

corSigProp

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

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)