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}