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)