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

module 1Lab.Type.Sigma where

private variable
  ℓ ℓ' ℓ'' : Level
  T A A' X X' Y Y' Z Z' : Type ℓ
  B P Q : A → Type ℓ
  C : (x : A) → B x → Type ℓ

Properties of Σ types🔗

This module contains properties of $Σ$ 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, and this is easy to prove directly, because paths in cubical type theory automatically inherit the structure of their domain types:

Σ-pathp≃
  : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
    {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  → (Σ[ p ∈ PathP A (x .fst) (y .fst) ]
      (PathP (λ i → B i (p i)) (x .snd) (y .snd)))
  ≃ (PathP (λ i → Σ (A i) (B i)) x y)

Σ-pathp≃ .fst = λ (p , q) i → p i , q i
Σ-pathp≃ .snd = is-iso→is-equiv λ where
  .is-iso.from p → (λ i → p i .fst) , λ i → p i .snd
  .is-iso.linv p → refl
  .is-iso.rinv p → refl

module Σ-pathp {ℓ ℓ'} {A : I → Type ℓ} {B : ∀ i → A i → Type ℓ'} {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)} = Equiv (Σ-pathp≃ {A = A} {B} {x} {y})

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) → Σ A P ≃ Σ A Q
Σ-ap-fst : (e : A ≃ A') → Σ A (B ∘ e .fst) ≃ Σ A' B

Σ-ap : (e : A ≃ A') → ((x : A) → P x ≃ Q (e .fst x)) → Σ A P ≃ Σ A' 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 = eqv where
  module pwise {i} = Equiv (pointwise i)

  eqv : (Σ _ P) ≃ (Σ _ Q)
  eqv .fst (i , x) = i , pwise.to x
  eqv .snd = is-iso→is-equiv λ where
    .is-iso.from (i , x) → i , pwise.from x
    .is-iso.linv (i , x) → ap₂ _,_ refl (pwise.η _)
    .is-iso.rinv (i , x) → ap₂ _,_ refl (pwise.ε _)

Σ-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.from p) renaming (fst to ρ; snd to σ)
      open Σ (Σ-pathp.from (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))) (∂ i) λ where
        k (i = i0) → ctrP (~ k)
        k (i = i1) → σ (~ k)
        k (k = i0) → b

      coh : PathP (λ i → PB (α≡ρ i) (b!≡s i) b) ctrP σ
      coh i j = fill (λ k → B (α≡ρ i (~ k))) (∂ i) (~ j) λ where
        k (i = i0) → ctrP (~ k)
        k (i = i1) → σ (~ k)
        k (k = i0) → b

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 ℓ} (bp : ∀ 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 λ where
  .is-iso.from   → ap fst
  .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:

  .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

Σ-set-square
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
  → {w x y z : Σ _ B}
  → (∀ x → is-set (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
Σ-set-square Bset sq i j .fst = sq i j
Σ-set-square Bset {p} {q} {s} {r} sq i j .snd =
  is-set→squarep (λ i j → Bset (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.from 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
  : (f : A → A')
  → ({x : A} → P x → Q (f x)) → Σ _ P → Σ _ Q
Σ-map f g (x , y) = f x , g y

Σ-map₂ : ({x : A} → P x → Q x) → Σ _ P → Σ _ Q
Σ-map₂ f (x , y) = (x , f y)

×-map : (A → A') → (X → X') → A × X → A' × X'
×-map f g (x , y) = (f x , g y)

×-map₁ : (A → A') → A × X → A' × X
×-map₁ f = ×-map f id

×-map₂ : (X → X') → A × X → A × X'
×-map₂ f = ×-map id f

_,ₚ_ = Σ-pathp
infixr 4 _,ₚ_

Σ-prop-pathp
  : ∀ {ℓ ℓ'} {A : I → Type ℓ} {B : ∀ i → A i → Type ℓ'}
  → (∀ i x → is-prop (B i x))
  → {x : Σ (A i0) (B i0)} {y : Σ (A i1) (B i1)}
  → PathP A (x .fst) (y .fst)
  → PathP (λ i → Σ (A i) (B i)) x y
Σ-prop-pathp bp {x} {y} p i =
  p i , is-prop→pathp (λ i → bp i (p i)) (x .snd) (y .snd) i

Σ-inj-set
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z}
  → is-set A
  → Path (Σ A B) (x , y) (x , z)
  → y ≡ z
Σ-inj-set {B = B} {y = y} {z} aset path =
  subst (λ e → e ≡ z) (ap (λ e → transport (ap B e) y) (aset _ _ _ _) ∙ transport-refl y)
    (from-pathp (ap snd path))

Σ-swap₂
  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : A → B → Type ℓ''}
  → (Σ[ x ∈ A ] Σ[ y ∈ B ] (C x y)) ≃ (Σ[ y ∈ B ] Σ[ x ∈ A ] (C x y))
Σ-swap₂ .fst (x , y , f) = y , x , f
Σ-swap₂ .snd .is-eqv y = contr (f .fst) (f .snd) where
  f = strict-fibres _ y
  -- agda can actually infer the inverse here, which is neat

×-swap
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
  → (A × B) ≃ (B × A)
×-swap .fst (x , y) = y , x
×-swap .snd .is-eqv y = contr (f .fst) (f .snd) where
  f = strict-fibres _ y

Σ-contr-eqv
  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
  → (c : is-contr A)
  → (Σ A B) ≃ B (c .centre)
Σ-contr-eqv {B = B} c .fst (_ , p) = subst B (sym (c .paths _)) p
Σ-contr-eqv {B = B} c .snd = is-iso→is-equiv λ where
  .is-iso.from x → _ , x
  .is-iso.rinv x → ap (λ e → subst B e x) (is-contr→is-set c _ _ _ _) ∙ transport-refl x
  .is-iso.linv x → Σ-path (c .paths _) (transport⁻transport (ap B (sym (c .paths (x .fst)))) (x .snd))

The universal property of sigma types🔗

Like all good type formers, $Σ$ types obey a universal property. First, observe that every pair of functions $f : (x : A) \to B x,$ $g : (x : A) \to C x (f x)$ induces a map $⟨ f, g ⟩ : (x : A) \to Σ (B x) (C x (f x))$

⟨_,_⟩
  : (f : (x : A) → B x)
  → (g : (x : A) → C x (f x))
  → (x : A) → Σ (B x) (C x)
⟨ f , g ⟩ x = f x , g x

Moreover, this map is part of an equivalence between functions $(x : A) \to Σ (B x) (C x (f x)$ into a $Σ$ type and pairs of functions into the components of the $Σ$ type.

Σ-Π-distrib
  : ((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-iso→is-equiv λ where
  .is-iso.from (f , g) → ⟨ f , g ⟩
  .is-iso.linv p → refl
  .is-iso.rinv p → refl

However, this isn’t the only universal property that $Σ$ types enjoy. Our previous universal property let us characterise maps into $Σ$ types: we also have a universal characterisation of maps out of $Σ$ types.

First, observe that we can pass between functions $(ab : Σ A B) \to C (π_{1} ab) (π_{2} ab)$ and functions $(a : A) \to (b : B a) \to C a b .$

curry : ((ab : Σ A B) → C (ab .fst) (ab .snd)) → (x : A) → (y : B x) → C x y
curry f a b = f (a , b)

uncurry : ((x : A) → (y : B x) → C x y) → (ab : Σ A B) → C (ab .fst) (ab .snd)
uncurry f (a , b) = f a b

We can then assemble these two maps into an equivalence.

Π-Σ-distrib
  : ((ab : Σ A B) → C (ab .fst) (ab .snd))
  ≃ (((x : A) → (y : B x) → C x y))
Π-Σ-distrib .fst = curry
Π-Σ-distrib .snd = is-iso→is-equiv λ where
  .is-iso.from → uncurry
  .is-iso.rinv f → refl
  .is-iso.linv f → refl

The type arithmetic of sigma types🔗

$Σ$ types are associative up to equivalence.

Σ-assoc : (Σ[ 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-iso→is-equiv λ where
  .is-iso.from ((x , y) , z) → x , y , z
  .is-iso.linv p → refl
  .is-iso.rinv p → refl