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