Martin Escardo, 30 April 2020

The structure identity principle and tools from the 2019 paper and links

https://arxiv.org/abs/1911.00580
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes

There are three submodules:

* sip
* sip-with-axioms
* sip-join

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module UF.SIP where

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv hiding (_≅_)
open import UF.Univalence
open import UF.EquivalenceExamples
open import UF.Subsingletons
open import UF.Embeddings
open import UF.Yoneda
open import UF.Retracts

module sip where

⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
⟨ X , s ⟩ = X

structure : {S : 𝓤 ̇ → 𝓥 ̇ } (A : Σ S) → S ⟨ A ⟩
structure (X , s) = s

canonical-map : {S : 𝓤 ̇ → 𝓥 ̇ }
(ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ )
(ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩))
{X : 𝓤 ̇ }
(s t : S X)
→ s ＝ t → ι (X , s) (X , t) (≃-refl X)
canonical-map ι ρ {X} s s (refl {s}) = ρ (X , s)

SNS : (𝓤 ̇ → 𝓥 ̇ ) → (𝓦 : Universe) → 𝓤 ⁺ ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇
SNS {𝓤} {𝓥} S 𝓦 = Σ ι ꞉ ((A B : Σ S) → (⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ ))
, Σ ρ ꞉ ((A : Σ S) → ι A A (≃-refl ⟨ A ⟩))
, ({X : 𝓤 ̇ } (s t : S X) → is-equiv (canonical-map ι ρ s t))

homomorphic : {S : 𝓤 ̇ → 𝓥 ̇ } → SNS S 𝓦
→ (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇
homomorphic (ι , ρ , θ) = ι

_≃[_]_ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → SNS S 𝓦 → Σ S → 𝓤 ⊔ 𝓦 ̇
A ≃[ σ ] B = Σ f ꞉ (⟨ A ⟩ → ⟨ B ⟩)
, Σ i ꞉ is-equiv f
, homomorphic σ A B (f , i)

Id→homEq : {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
→ (A B : Σ S) → (A ＝ B) → (A ≃[ σ ] B)
Id→homEq (_ , ρ , _) A A (refl {A}) = id , id-is-equiv ⟨ A ⟩ , ρ A

homomorphism-lemma : {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
(A B : Σ S) (p : ⟨ A ⟩ ＝ ⟨ B ⟩)
→
(transport S p (structure A) ＝ structure B)
≃  homomorphic σ A B (idtoeq ⟨ A ⟩ ⟨ B ⟩ p)
homomorphism-lemma (ι , ρ , θ) (X , s) (X , t) (refl {X}) = γ
where
γ : (s ＝ t) ≃ ι (X , s) (X , t) (≃-refl X)
γ = (canonical-map ι ρ s t , θ s t)

characterization-of-＝ : is-univalent 𝓤
→ {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
→ (A B : Σ S)

→ (A ＝ B) ≃ (A ≃[ σ ] B)
characterization-of-＝ ua {S} σ A B =
(A ＝ B)                                                            ≃⟨ i ⟩
(Σ p ꞉ ⟨ A ⟩ ＝ ⟨ B ⟩ , transport S p (structure A) ＝ structure B) ≃⟨ ii ⟩
(Σ p ꞉ ⟨ A ⟩ ＝ ⟨ B ⟩ , ι A B (idtoeq ⟨ A ⟩ ⟨ B ⟩ p))               ≃⟨ iii ⟩
(Σ e ꞉ ⟨ A ⟩ ≃ ⟨ B ⟩ , ι A B e)                                     ≃⟨ iv ⟩
(A ≃[ σ ] B)                                                        ■
where
ι   = homomorphic σ
i   = Σ-＝-≃
ii  = Σ-cong (homomorphism-lemma σ A B)
iii = Σ-change-of-variable (ι A B) (idtoeq ⟨ A ⟩ ⟨ B ⟩) (ua ⟨ A ⟩ ⟨ B ⟩)
iv  = Σ-assoc

Id→homEq-is-equiv : (ua : is-univalent 𝓤) {S : 𝓤 ̇ → 𝓥 ̇ } (σ : SNS S 𝓦)
→ (A B : Σ S) → is-equiv (Id→homEq σ A B)
Id→homEq-is-equiv ua {S} σ A B = γ
where
h : (A B : Σ S) → Id→homEq σ A B ∼ ⌜ characterization-of-＝ ua σ A B ⌝
h A A (refl {A}) = refl

γ : is-equiv (Id→homEq σ A B)
γ = equiv-closed-under-∼ _ _
(⌜⌝-is-equiv (characterization-of-＝ ua σ A B))
(h A B)

module _ {S : 𝓤 ̇ → 𝓥 ̇ }
(ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦 ̇ )
(ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩))
{X : 𝓤 ̇ }
where

canonical-map-charac : (s t : S X) (p : s ＝ t)
→ canonical-map ι ρ s t p
＝ transport (λ - → ι (X , s) (X , -) (≃-refl X)) p (ρ (X , s))
canonical-map-charac s t p = (yoneda-lemma s (λ t → ι (X , s) (X , t) (≃-refl X)) (canonical-map ι ρ s) t p)⁻¹

when-canonical-map-is-equiv : ((s t : S X) → is-equiv (canonical-map ι ρ s t))
⇔ ((s : S X) → ∃! t ꞉ S X , ι (X , s) (X , t) (≃-refl X))
when-canonical-map-is-equiv = (λ e s → Yoneda-Theorem-back  s (τ s) (e s)) ,
(λ φ s → Yoneda-Theorem-forth s (τ s) (φ s))
where
A = λ s t → ι (X , s) (X , t) (≃-refl X)
τ = canonical-map ι ρ

canonical-map-equiv-criterion : ((s t : S X)
→ (s ＝ t) ≃ ι (X , s) (X , t) (≃-refl X))
→ (s t : S X) → is-equiv (canonical-map ι ρ s t)
canonical-map-equiv-criterion φ s = fiberwise-equiv-criterion'
(λ t → ι (X , s) (X , t) (≃-refl X))
s (φ s) (canonical-map ι ρ s)

canonical-map-equiv-criterion' : ((s t : S X)
→ ι (X , s) (X , t) (≃-refl X) ◁ (s ＝ t))
→ (s t : S X) → is-equiv (canonical-map ι ρ s t)
canonical-map-equiv-criterion' φ s = fiberwise-equiv-criterion
(λ t → ι (X , s) (X , t) (≃-refl X))
s (φ s) (canonical-map ι ρ s)

module sip-with-axioms where

open sip

[_] : {S : 𝓤 ̇ → 𝓥 ̇ } {axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ }
→ (Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s) → Σ S
[ X , s , _ ] = (X , s)

⟪_⟫ : {S : 𝓤 ̇ → 𝓥 ̇ } {axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ }
→ (Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s) → 𝓤 ̇
⟪ X , _ , _ ⟫ = X

add-axioms : {S : 𝓤 ̇ → 𝓥 ̇ }
(axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ )
→ ((X : 𝓤 ̇ ) (s : S X) → is-prop (axioms X s))
→ SNS S 𝓣
→ SNS (λ X → Σ s ꞉ S X , axioms X s) 𝓣
add-axioms {𝓤} {𝓥} {𝓦} {𝓣} {S} axioms i (ι , ρ , θ) = ι' , ρ' , θ'
where
S' : 𝓤 ̇ → 𝓥 ⊔ 𝓦  ̇
S' X = Σ s ꞉ S X , axioms X s

ι' : (A B : Σ S') → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓣 ̇
ι' A B = ι [ A ] [ B ]

ρ' : (A : Σ S') → ι' A A (≃-refl ⟨ A ⟩)
ρ' A = ρ [ A ]

θ' : {X : 𝓤 ̇ } (s' t' : S' X) → is-equiv (canonical-map ι' ρ' s' t')
θ' {X} (s , a) (t , b) = γ
where
π : S' X → S X
π (s , _) = s

j : is-embedding π
j = pr₁-is-embedding (i X)

k : {s' t' : S' X} → is-equiv (ap π {s'} {t'})
k {s'} {t'} = embedding-gives-embedding' π j s' t'

l : canonical-map ι' ρ' (s , a) (t , b)
∼ canonical-map ι ρ s t ∘ ap π {s , a} {t , b}

l (refl {s , a}) = 𝓻𝓮𝒻𝓵 (ρ (X , s))

e : is-equiv (canonical-map ι ρ s t ∘ ap π {s , a} {t , b})
e = ∘-is-equiv k (θ s t)

γ : is-equiv (canonical-map ι' ρ' (s , a) (t , b))
γ = equiv-closed-under-∼ _ _ e l

characterization-of-＝-with-axioms : is-univalent 𝓤
→ {S : 𝓤 ̇ → 𝓥 ̇ }
(σ : SNS S 𝓣)
(axioms : (X : 𝓤 ̇ ) → S X → 𝓦 ̇ )
→ ((X : 𝓤 ̇ ) (s : S X) → is-prop (axioms X s))
→ (A B : Σ X ꞉ 𝓤 ̇ , Σ s ꞉ S X , axioms X s)
→ (A ＝ B) ≃ ([ A ] ≃[ σ ] [ B ])
characterization-of-＝-with-axioms ua σ axioms i =
characterization-of-＝ ua (add-axioms axioms i σ)

module sip-join where

technical-lemma :

{X : 𝓤 ̇ } {A : X → X → 𝓥 ̇ }
{Y : 𝓦 ̇ } {B : Y → Y → 𝓣 ̇ }
(f : (x₀ x₁ : X) → x₀ ＝ x₁ → A x₀ x₁)
(g : (y₀ y₁ : Y) → y₀ ＝ y₁ → B y₀ y₁)
→ ((x₀ x₁ : X) → is-equiv (f x₀ x₁))
→ ((y₀ y₁ : Y) → is-equiv (g y₀ y₁))

→ ((x₀ , y₀) (x₁ , y₁) : X × Y) →
is-equiv (λ (p : (x₀ , y₀) ＝ (x₁ , y₁)) → f x₀ x₁ (ap pr₁ p) ,
g y₀ y₁ (ap pr₂ p))

technical-lemma {𝓤} {𝓥} {𝓦} {𝓣} {X} {A} {Y} {B} f g i j (x₀ , y₀) = γ
where
module _ ((x₁ , y₁) : X × Y) where
r : (x₀ , y₀) ＝ (x₁ , y₁) → A x₀ x₁ × B y₀ y₁
r p = f x₀ x₁ (ap pr₁ p) , g y₀ y₁ (ap pr₂ p)

f' : (a : A x₀ x₁) → x₀ ＝ x₁
f' = inverse (f x₀ x₁) (i x₀ x₁)

g' : (b : B y₀ y₁) → y₀ ＝ y₁
g' = inverse (g y₀ y₁) (j y₀ y₁)

s : A x₀ x₁ × B y₀ y₁ → (x₀ , y₀) ＝ (x₁ , y₁)
s (a , b) = to-×-＝ (f' a) (g' b)

η : (c : A x₀ x₁ × B y₀ y₁) → r (s c) ＝ c
η (a , b) =
r (s (a , b))                               ＝⟨ refl ⟩
r (to-×-＝  (f' a) (g' b))                  ＝⟨ refl ⟩
(f x₀ x₁ (ap pr₁ (to-×-＝ (f' a) (g' b))) ,
g y₀ y₁ (ap pr₂ (to-×-＝ (f' a) (g' b))))  ＝⟨ ii ⟩
(f x₀ x₁ (f' a) , g y₀ y₁ (g' b))           ＝⟨ iii ⟩
a , b                                       ∎
where
ii  = ap₂ (λ p q → f x₀ x₁ p , g y₀ y₁ q)
(ap-pr₁-to-×-＝ (f' a) (g' b))
(ap-pr₂-to-×-＝ (f' a) (g' b))
iii = to-×-＝ (inverses-are-sections (f x₀ x₁) (i x₀ x₁) a)
(inverses-are-sections (g y₀ y₁) (j y₀ y₁) b)

γ : ∀ z₁ → is-equiv (r z₁)
γ = nats-with-sections-are-equivs (x₀ , y₀) r λ z₁ → (s z₁ , η z₁)

variable
𝓥₀ 𝓥₁ 𝓦₀ 𝓦₁ : Universe

open sip

⟪_⟫ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
→ (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → 𝓤 ̇
⟪ X , s₀ , s₁ ⟫ = X

[_]₀ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
→ (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → Σ S₀
[ X , s₀ , s₁ ]₀ = (X , s₀)

[_]₁ : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
→ (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X) → Σ S₁
[ X , s₀ , s₁ ]₁ = (X , s₁)

join : {S₀ : 𝓤 ̇ → 𝓥₀ ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
→ SNS S₀ 𝓦₀
→ SNS S₁ 𝓦₁
→ SNS (λ X → S₀ X × S₁ X) (𝓦₀ ⊔ 𝓦₁)
join {𝓤} {𝓥₀} {𝓥₁} {𝓦₀} {𝓦₁} {S₀} {S₁} (ι₀ , ρ₀ , θ₀) (ι₁ , ρ₁ , θ₁) = ι , ρ , θ
where
S : 𝓤 ̇ → 𝓥₀ ⊔ 𝓥₁ ̇
S X = S₀ X × S₁ X

ι : (A B : Σ S) → ⟨ A ⟩ ≃ ⟨ B ⟩ → 𝓦₀ ⊔ 𝓦₁ ̇
ι A B e = ι₀ [ A ]₀ [ B ]₀ e  ×  ι₁ [ A ]₁ [ B ]₁ e

ρ : (A : Σ S) → ι A A (≃-refl ⟨ A ⟩)
ρ A = (ρ₀ [ A ]₀ , ρ₁ [ A ]₁)

θ : {X : 𝓤 ̇ } (s t : S X) → is-equiv (canonical-map ι ρ s t)
θ {X} (s₀ , s₁) (t₀ , t₁) = γ
where
c : (p : s₀ , s₁ ＝ t₀ , t₁) → ι₀ (X , s₀) (X , t₀) (≃-refl X)
× ι₁ (X , s₁) (X , t₁) (≃-refl X)

c p = (canonical-map ι₀ ρ₀ s₀ t₀ (ap pr₁ p) ,
canonical-map ι₁ ρ₁ s₁ t₁ (ap pr₂ p))

i : is-equiv c
i = technical-lemma
(canonical-map ι₀ ρ₀)
(canonical-map ι₁ ρ₁)
θ₀ θ₁ (s₀ , s₁) (t₀ , t₁)

e : canonical-map ι ρ (s₀ , s₁) (t₀ , t₁) ∼ c
e (refl {s₀ , s₁}) = 𝓻𝓮𝒻𝓵 (ρ₀ (X , s₀) , ρ₁ (X , s₁))

γ : is-equiv (canonical-map ι ρ (s₀ , s₁) (t₀ , t₁))
γ = equiv-closed-under-∼ _ _ i e

_≃⟦_,_⟧_ : {S₀ : 𝓤 ̇ → 𝓥 ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
→ (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)
→ SNS S₀ 𝓦₀
→ SNS S₁ 𝓦₁
→ (Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)
→ 𝓤 ⊔ 𝓦₀ ⊔ 𝓦₁ ̇
A ≃⟦ σ₀ , σ₁ ⟧ B = Σ f ꞉ (⟪ A ⟫ → ⟪ B ⟫)
, Σ i ꞉ is-equiv f , homomorphic σ₀ [ A ]₀ [ B ]₀ (f , i)
× homomorphic σ₁ [ A ]₁ [ B ]₁ (f , i)

characterization-of-join-＝ : is-univalent 𝓤
→ {S₀ : 𝓤 ̇ → 𝓥 ̇ } {S₁ : 𝓤 ̇ → 𝓥₁ ̇ }
(σ₀ : SNS S₀ 𝓦₀)  (σ₁ : SNS S₁ 𝓦₁)
(A B : Σ X ꞉ 𝓤 ̇ , S₀ X × S₁ X)
→ (A ＝ B) ≃ (A ≃⟦ σ₀ , σ₁ ⟧ B)
characterization-of-join-＝ ua σ₀ σ₁ = characterization-of-＝ ua (join σ₀ σ₁)

\end{code}