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 --safe --without-K #-}

module UF.SIP where

open import MLTT.Spartan
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Retracts
open import UF.Subsingletons
open import UF.Univalence
open import UF.Yoneda

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 (c s) (e s)) ,
                                (λ φ s → Yoneda-Theorem-forth s (c s) (φ s))
   where
    c = 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 : X × Y) → 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₀ , s₁) t@(t₀ , t₁) = γ
    where
     c : (p : s ＝ 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 t

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

     γ : is-equiv (canonical-map ι ρ s 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}