module 1Lab.Type.Sigma where
private variable
: Level
ℓ ℓ₁ : Type ℓ
A A' X X' Y Y' Z Z' : A → Type ℓ
B P Q : (x : A) → B x → Type ℓ C
Properties of Σ types🔗
This module contains properties of types, not necessarily organised in any way.
Universal property🔗
If we have a pair of maps and then there exists a unique universal map that commutes with the projections. This is essentially a dependently typed version of the universal property of products.
_,_⟩ : (f : (x : A) → B x) → (g : (x : A) → C x (f x)) → (x : A) → Σ (B x) (C x)
⟨= f x , g x
⟨ f , g ⟩ x
⟨⟩-unique: ∀ {f : (x : A) → B x} {g : (x : A) → C x (f x)}
→ (h : (x : A) → Σ (B x) (C x))
→ (p : fst ∘ h ≡ f)
→ PathP (λ i → (x : A) → C x (p i x)) (snd ∘ h) g
→ h ≡ ⟨ f , g ⟩
= p i x , q i x ⟨⟩-unique h p q i x
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)
≃
.fst = λ (p , q) i → p i , q i
Σ-pathp≃ .snd = is-iso→is-equiv λ where
Σ-pathp≃ .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:
: ((x : A) → P x ≃ Q x) → Σ A P ≃ Σ A Q
Σ-ap-snd : (e : A ≃ A') → Σ A (B ∘ e .fst) ≃ Σ A' B
Σ-ap-fst
: (e : A ≃ A') → ((x : A) → P x ≃ Q (e .fst x)) → Σ A P ≃ Σ A' Q
Σ-ap = Σ-ap-snd e' ∙e Σ-ap-fst e Σ-ap e e'
The proofs of these theorems are not very enlightening, but they are included for completeness.
{A = A} {P = P} {Q = Q} pointwise = eqv where
Σ-ap-snd module pwise {i} = Equiv (pointwise i)
: (Σ _ P) ≃ (Σ _ Q)
eqv .fst (i , x) = i , pwise.to x
eqv .snd = is-iso→is-equiv λ where
eqv .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.ε _)
{A = A} {A' = A'} {B = B} e = intro , isEqIntro where
Σ-ap-fst : Σ _ (B ∘ e .fst) → Σ _ B
intro (a , b) = e .fst a , b
intro
: is-equiv intro
isEqIntro .is-eqv x = contr ctr isCtr where
isEqIntro : ∀ {x y} → x ≡ y → B x → B y → Type _
PB = PathP (λ i → B (p i))
PB p
open Σ x renaming (fst to a'; snd to b)
open Σ (e .snd .is-eqv a' .is-contr.centre) renaming (fst to ctrA; snd to α)
: B (e .fst ctrA)
ctrB = subst B (sym α) b
ctrB
: PB α ctrB b
ctrP = coe1→i (λ i → B (α i)) i b
ctrP i
: fibre intro x
ctr = (ctrA , ctrB) , Σ-pathp α ctrP
ctr
: ∀ y → ctr ≡ y
isCtr ((r , s) , p) = λ i → (a≡r i , b!≡s i) , Σ-pathp (α≡ρ i) (coh i) where
isCtr 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 α≡ρ)
: PB (ap (e .fst) a≡r) ctrB s
b!≡s = comp (λ k → B (α≡ρ i (~ k))) (∂ i) λ where
b!≡s i (i = i0) → ctrP (~ k)
k (i = i1) → σ (~ k)
k (k = i0) → b
k
: PathP (λ i → PB (α≡ρ i) (b!≡s i) b) ctrP σ
coh = fill (λ k → B (α≡ρ i (~ k))) (∂ i) (~ j) λ where
coh i j (i = i0) → ctrP (~ k)
k (i = i1) → σ (~ k)
k (k = i0) → b
k
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
Σ-assoc → (Σ[ x ∈ A ] Σ[ y ∈ B x ] C x y) ≃ (Σ[ x ∈ Σ _ B ] (C (x .fst) (x .snd)))
.fst (x , y , z) = (x , y) , z
Σ-assoc .snd .is-eqv ((x , y), z) = contr (fib .fst) (fib .snd)
Σ-assoc where fib = strict-fibres _ ((x , y) , z)
: ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {C : (x : A) → B x → Type ℓ''}
Σ-Π-distrib → ((x : A) → Σ[ y ∈ B x ] C x y)
(Σ[ f ∈ ((x : A) → B x) ] ((x : A) → C x (f x)))
≃ .fst f = (fst ∘ f) , (snd ∘ f)
Σ-Π-distrib .snd .is-eqv (f , r) = contr (fib .fst) (fib .snd)
Σ-Π-distrib where fib = strict-fibres (λ h → ⟨ h .fst , h .snd ⟩) (f , r)
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
{x} {y} p i =
Σ-prop-path bp (λ i → bp (p i)) (x .snd) (y .snd) i p i , is-prop→pathp
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})
{x} {y} = is-iso→is-equiv λ where
Σ-prop-path-is-equiv bp .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-is-equiv bp Σ-prop-path≃ 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
.fst = sq i j
Σ-prop-square Bprop sq i j {p} {q} {s} {r} sq i j .snd =
Σ-prop-square Bprop (λ i j → Bprop (sq i j))
is-prop→squarep (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
.fst = sq i j
Σ-set-square Bset sq i j {p} {q} {s} {r} sq i j .snd =
Σ-set-square Bset (λ i j → Bset (sq i j))
is-set→squarep (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
:
: {B : A → Type ℓ} → (∀ x → is-contr (B x)) → Σ _ B ≃ A
Σ-contract = Iso→Equiv the-iso where
Σ-contract bcontr : 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 the-iso
Σ-map: (f : A → A')
→ ({x : A} → P x → Q (f x)) → Σ _ P → Σ _ Q
(x , y) = f x , g y
Σ-map f g
: ({x : A} → P x → Q x) → Σ _ P → Σ _ Q
Σ-map₂ (x , y) = (x , f y)
Σ-map₂ f
: (A → A') → (X → X') → A × X → A' × X'
×-map (x , y) = (f x , g y)
×-map f g
: (A → A') → A × X → A' × X
×-map₁ = ×-map f id
×-map₁ f
: (X → X') → A × X → A × X'
×-map₂ = ×-map id f ×-map₂ 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
{x} {y} p i =
Σ-prop-pathp bp (λ i → bp i (p i)) (x .snd) (y .snd) i
p i , is-prop→pathp
Σ-inj-set: ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z}
→ is-set A
→ Path (Σ A B) (x , y) (x , z)
→ y ≡ z
{B = B} {y = y} {z} aset path =
Σ-inj-set (λ e → e ≡ z) (ap (λ e → transport (ap B e) y) (aset _ _ _ _) ∙ transport-refl y)
subst (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))
.fst (x , y , f) = y , x , f
Σ-swap₂ .snd .is-eqv y = contr (f .fst) (f .snd) where
Σ-swap₂ = strict-fibres _ y
f -- agda can actually infer the inverse here, which is neat
×-swap: ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
→ (A × B) ≃ (B × A)
.fst (x , y) = y , x
×-swap .snd .is-eqv y = contr (f .fst) (f .snd) where
×-swap = strict-fibres _ y
f
Σ-contr-eqv: ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
→ (c : is-contr A)
→ (Σ A B) ≃ B (c .centre)
{B = B} c .fst (_ , p) = subst B (sym (c .paths _)) p
Σ-contr-eqv {B = B} c .snd = is-iso→is-equiv λ where
Σ-contr-eqv .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))
module _ {ℓ ℓ' ℓ''} {X : Type ℓ} {Y : X → Type ℓ'} {Z : (x : X) → Y x → Type ℓ''} where
: ((p : Σ X Y) → Z (p .fst) (p .snd)) → (x : X) → (y : Y x) → Z x y
curry = f (a , b)
curry f a b
: ((x : X) → (y : Y x) → Z x y) → (p : Σ X Y) → Z (p .fst) (p .snd)
uncurry (a , b) = f a b uncurry f