open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Type.Sigma where

Properties of Ξ£ typesπŸ”—

This module contains properties of Ξ£\Sigma types, not necessarily organised in any way.

Groupoid structureπŸ”—

The first thing we prove is that paths in sigmas are sigmas of paths. The type signatures make it clearer:

Ξ£-pathp-iso : {A : I β†’ Type β„“} {B : (i : I) β†’ A i β†’ Type ℓ₁}
              {x : Ξ£ (B i0)} {y : Ξ£ (B i1)}
            β†’ Iso (Ξ£[ p ∈ PathP A (x .fst) (y .fst) ]
                    (PathP (Ξ» i β†’ B i (p i)) (x .snd) (y .snd)))
                  (PathP (Ξ» i β†’ Ξ£ (B i)) x y)

Ξ£-path-iso : {x y : Ξ£ B}
           β†’ Iso (Ξ£[ p ∈ x .fst ≑ y .fst ] (subst B p (x .snd) ≑ y .snd))
                 (x ≑ y)

The first of these, using a dependent path, is easy to prove directly, because paths in cubical type theory automatically inherit the structure of their domain types. The second is a consequence of the first, using the fact that PathPs and paths over a transport are the same.

fst Ξ£-pathp-iso (p , q) i = p i , q i
is-iso.inv (snd Ξ£-pathp-iso) p = (Ξ» i β†’ p i .fst) , (Ξ» i β†’ p i .snd)
is-iso.rinv (snd Ξ£-pathp-iso) x = refl
is-iso.linv (snd Ξ£-pathp-iso) x = refl

Ξ£-path-iso {B = B} {x} {y} =
  transport (Ξ» i β†’ Iso (Ξ£[ p ∈ x .fst ≑ y .fst ]
                         (PathP≑Path (Ξ» j β†’ B (p j)) (x .snd) (y .snd) i))
                       (x ≑ y))
            Ξ£-pathp-iso

Closure under equivalencesπŸ”—

Univalence automatically implies that every type former respects equivalences. However, this theorem is limited to equivalences between types in the same universe. Thus, we provide Ξ£-ap-fst, Ξ£-ap-snd, and Ξ£-ap, which allows one to perturb a Ξ£ by equivalences across levels:

Ξ£-ap-snd : ((x : A) β†’ P x ≃ Q x) β†’ Ξ£ P ≃ Ξ£ Q
Ξ£-ap-fst : (e : A ≃ A') β†’ Ξ£ (B ∘ e .fst) ≃ Ξ£ B

Ξ£-ap : (e : A ≃ A') β†’ ((x : A) β†’ P x ≃ Q (e .fst x)) β†’ Ξ£ P ≃ Ξ£ Q
Ξ£-ap e e' = Ξ£-ap-snd e' βˆ™e Ξ£-ap-fst e
The proofs of these theorems are not very enlightening, but they are included for completeness.
Σ-ap-snd {A = A} {P = P} {Q = Q} pointwise = Iso→Equiv morp where
  pwise : (x : A) β†’ Iso (P x) (Q x)
  pwise x = _ , is-equiv→is-iso (pointwise x .snd)

  morp : Iso (Ξ£ P) (Ξ£ Q)
  fst morp (i , x) = i , pointwise i .fst x
  is-iso.inv (snd morp) (i , x) = i , pwise i .snd .is-iso.inv x
  is-iso.rinv (snd morp) (i , x) = apβ‚‚ _,_ refl (pwise i .snd .is-iso.rinv _)
  is-iso.linv (snd morp) (i , x) = apβ‚‚ _,_ refl (pwise i .snd .is-iso.linv _)

Ξ£-ap-fst {A = A} {A' = A'} {B = B} e = intro , isEqIntro
 where
  intro : Ξ£ (B ∘ e .fst) β†’ Ξ£ B
  intro (a , b) = e .fst a , b

  isEqIntro : is-equiv intro
  isEqIntro .is-eqv x = contr ctr isCtr where
    PB : βˆ€ {x y} β†’ x ≑ y β†’ B x β†’ B y β†’ Type _
    PB p = PathP (Ξ» i β†’ B (p i))

    open Ξ£ x renaming (fst to a'; snd to b)
    open Ξ£ (e .snd .is-eqv a' .is-contr.centre) renaming (fst to ctrA; snd to Ξ±)

    ctrB : B (e .fst ctrA)
    ctrB = subst B (sym Ξ±) b

    ctrP : PB Ξ± ctrB b
    ctrP i = coe1β†’i (Ξ» i β†’ B (Ξ± i)) i b

    ctr : fibre intro x
    ctr = (ctrA , ctrB) , Ξ£-pathp Ξ± ctrP

    isCtr : βˆ€ y β†’ ctr ≑ y
    isCtr ((r , s) , p) = Ξ» i β†’ (a≑r i , b!≑s i) , Ξ£-pathp (α≑ρ i) (coh i) where
      open Ξ£ (Ξ£-pathp-iso .snd .is-iso.inv p) renaming (fst to ρ; snd to Οƒ)
      open Ξ£ (Ξ£-pathp-iso .snd .is-iso.inv (e .snd .is-eqv a' .is-contr.paths (r , ρ))) renaming (fst to a≑r; snd to α≑ρ)

      b!≑s : PB (ap (e .fst) a≑r) ctrB s
      b!≑s i = comp (Ξ» k β†’ B (α≑ρ i (~ k))) (Ξ» k β†’ (Ξ»
        { (i = i0) β†’ ctrP (~ k)
        ; (i = i1) β†’ Οƒ (~ k)
        })) b

      coh : PathP (Ξ» i β†’ PB (α≑ρ i) (b!≑s i) b) ctrP Οƒ
      coh i j = fill (Ξ» k β†’ B (α≑ρ i (~ k))) (Ξ» k β†’ (Ξ»
        { (i = i0) β†’ ctrP (~ k)
        ; (i = i1) β†’ Οƒ (~ k)
        })) (inS b) (~ j)

Ξ£-assoc : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : A β†’ Type β„“'} {C : (x : A) β†’ B x β†’ Type β„“''}
        β†’ (Ξ£[ x ∈ A ] Ξ£[ y ∈ B x ] C x y) ≃ (Ξ£[ x ∈ Ξ£ B ] (C (x .fst) (x .snd)))
Ξ£-assoc .fst (x , y , z) = (x , y) , z
Ξ£-assoc .snd .is-eqv y .centre = strict-fibres (Ξ» { ((x , y) , z) β†’ x , y , z}) y .fst
Ξ£-assoc .snd .is-eqv y .paths = strict-fibres (Ξ» { ((x , y) , z) β†’ x , y , z}) y .snd

Ξ£-Ξ -distrib : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : A β†’ Type β„“'} {C : (x : A) β†’ B x β†’ Type β„“''}
            β†’ ((x : A) β†’ Ξ£[ y ∈ B x ] C x y)
            ≃ (Ξ£[ f ∈ ((x : A) β†’ B x) ] ((x : A) β†’ C x (f x)))
Ξ£-Ξ -distrib .fst f = (Ξ» x β†’ f x .fst) , Ξ» x β†’ f x .snd
Ξ£-Ξ -distrib .snd .is-eqv y .centre = strict-fibres (Ξ» f x β†’ f .fst x , f .snd x) y .fst
Ξ£-Ξ -distrib .snd .is-eqv y .paths = strict-fibres (Ξ» f x β†’ f .fst x , f .snd x) y .snd

Paths in subtypesπŸ”—

When P is a family of propositions, it is sound to regard Σ[ x ∈ A ] (P x) as a subtype of A. This is because identification in the subtype is characterised uniquely by identification of the first projections:

Ξ£-prop-path : {B : A β†’ Type β„“}
            β†’ (βˆ€ x β†’ is-prop (B x))
            β†’ {x y : Ξ£ B}
            β†’ (x .fst ≑ y .fst) β†’ x ≑ y
Σ-prop-path bp {x} {y} p i = p i , is-prop→pathp (λ i → bp (p i)) (x .snd) (y .snd) i

The proof that this is an equivalence uses a cubical argument, but the gist of it is that since B is a family of propositions, it really doesn’t matter where we get our equality of B-s from - whether it was from the input, or from Σ≑Path.

Ξ£-prop-path-is-equiv
  : {B : A β†’ Type β„“}
  β†’ (bp : βˆ€ x β†’ is-prop (B x))
  β†’ {x y : Ξ£ B}
  β†’ is-equiv (Ξ£-prop-path bp {x} {y})
Σ-prop-path-is-equiv bp {x} {y} = is-iso→is-equiv isom where
  isom : is-iso _
  isom .is-iso.inv = ap fst
  isom .is-iso.linv p = refl

The inverse is the action on paths of the first projection, which lets us conclude x .fst ≑ y .fst from x ≑ y. This is a left inverse to Ξ£-prop-path on the nose. For the other direction, we have the aforementioned cubical argument:

  isom .is-iso.rinv p i j =
    p j .fst , is-prop→pathp (λ k → Path-is-hlevel 1 (bp (p k .fst))
                                      {x = Ξ£-prop-path bp {x} {y} (ap fst p) k .snd}
                                      {y = p k .snd})
                             refl refl j i

Since Ξ£-prop-path is an equivalence, this implies that its inverse, ap fst, is also an equivalence; This is precisely what it means for fst to be an embedding.

There is also a convenient packaging of the previous two definitions into an equivalence:

Ξ£-prop-path≃ : {B : A β†’ Type β„“}
             β†’ (βˆ€ x β†’ is-prop (B x))
             β†’ {x y : Ξ£ B}
             β†’ (x .fst ≑ y .fst) ≃ (x ≑ y)
Ξ£-prop-path≃ bp = Ξ£-prop-path bp , Ξ£-prop-path-is-equiv bp

Ξ£-prop-square
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'}
  β†’ {w x y z : Ξ£ B}
  β†’ (βˆ€ x β†’ is-prop (B x))
  β†’ {p : x ≑ w} {q : x ≑ y} {s : w ≑ z} {r : y ≑ z}
  β†’ Square (ap fst p) (ap fst q) (ap fst s) (ap fst r)
  β†’ Square p q s r
Ξ£-prop-square Bprop sq i j .fst = sq i j
Ξ£-prop-square Bprop {p} {q} {s} {r} sq i j .snd =
  is-prop→squarep (λ i j → Bprop (sq i j))
    (ap snd p) (ap snd q) (ap snd s) (ap snd r) i j

Dependent sums of contractiblesπŸ”—

If B is a family of contractible types, then Ξ£ B ≃ A:

Ξ£-contract : {B : A β†’ Type β„“} β†’ (βˆ€ x β†’ is-contr (B x)) β†’ Ξ£ B ≃ A
Σ-contract bcontr = Iso→Equiv the-iso where
  the-iso : Iso _ _
  the-iso .fst (a , b) = a
  the-iso .snd .is-iso.inv x = x , bcontr _ .centre
  the-iso .snd .is-iso.rinv x = refl
  the-iso .snd .is-iso.linv (a , b) i = a , bcontr a .paths b i
Ξ£-mapβ‚‚ : ({x : A} β†’ P x β†’ Q x) β†’ Ξ£ P β†’ Ξ£ Q
Ξ£-mapβ‚‚ f (x , y) = (x , f y)