CONTEXT SPACES

-type is a space that contains dependent pairs where type of the second element depends on the value of the first element. As only one point of fiber domain present in every defined pair, -type is also a dependent sum, where fiber base is a disjoint union.

Spaces of dependent pairs are using in type theory to model cartesian products, disjoint sums, fiber bundles, vector spaces, telescopes, lenses, contexts, objects, algebras, ∃-type, etc.

Formation

(-Formation, Dependent Sum). The dependent sum type is indexed over type in the sense of coproduct or disjoint union, where only one fiber codomain is present in pair.

def Sigma (A: U) (B: A → U) : U
 := Σ (x: A), B(x)

Introduction

(Dependent Pair). The dependent pair constructor is a way to create indexed pair over type in the sense of coproduct or disjoint union.

def pair (A: U) (B: A → U) (a: A) (b: B a)
  : Sigma A B := (a, b)

Elimination

(Dependent Projections). The dependent projections and are pair deconstructors.

def pr₁ (A: U) (B: A → U) (x: Sigma A B)
  : A := x.1
def pr₂ (A: U) (B: A → U) (x: Sigma A B)
  : B (pr₁ A B x) := x.2

If you want to access deep sigma a series of accessors should be applied followed by .

(-Induction Principle). States that if predicate holds for two projections then predicate holds for total space.

def Σ-ind (A : U) (B : A -> U)
    (C : Π (s: Σ (x: A), B x), U) 
    (g: Π (x: A) (y: B x), C (x,y))
    (p: Σ (x: A), B x) : C p := g p.1 p.2

Computation

(-Computation).

def Σ-β₁ (A : U) (B : A → U) (a : A) (b : B a)
  : Path A a (pr₁ A B (a ,b)) := idp A a

def Σ-β₂ (A : U) (B : A → U) (a : A) (b : B a)
  : Path (B a) b (pr₂ A B (a, b)) := idp (B a) b

Uniqueness

(-Uniqueness).

def Σ-η (A : U) (B : A → U) (p : Sigma A B)
  : Path (Sigma A B) p (pr₁ A B p, pr₂ A B p)
 := idp  (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 .

def ac (A B: U) (R: A -> B -> U)
    (g: Π (x: A), Σ (y: B), R x y)
  : Σ (f: A -> B), Π (x: A), R x (f x)
 := (\(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.

def total (A:U) (B C : A -> U)
    (f : Π (x:A), B x -> C x)
    (w: Σ(x: A), B x)
  : Σ (x: A), C x := (w.1,f (w.1) (w.2))

(Path Between Sigmas). Path between two sigmas could be decomposed to sigma of two paths and .

def funDepTr (A: U) (P: A -> U) (a0 a1: A)
    (p: PathP (<_>A) a0 a1) (u0: P a0) (u1: P a1)
  : PathP (<_>U) (PathP (<i> P (p @ i)) u0 u1)
    (PathP (<_>P a1) (hcomp (P a1) 0 (λ (k : I), [])
    (transp (<i> P (p @ i)) 0 u0)) u1)
 := <j> PathP (<i> P (p @ j \/ i)) (comp (\(i:I),
    P (p @ j /\ i)) -j (\(k: I),
    [(j = 0) -> u0 ]) (inc (P a0) -j u0)) u1

def pathSig (A: U) (P: A -> U)
    (t u: Σ (x: A), P x) (p: PathP (<_>A) t.1 u.1)
  : PathP (<_>U) (PathP (<i>P (p @ i)) t.2 u.2) 
          (PathP (<_>P u.1)
                 (hcomp (P u.1) 0 
                   (λ(k:I),[]) (transp (<i> P (p @ i))
                      0 t.2)) u.2)
                   := funDepTr A P t.1 u.1 p 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 (p@i)) 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 (p@i)) 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)