Martin Escardo, 14 Feb 2024.

Generalization of UF.SIP to characterize equality of Σ-types,
suggested by Ian Ray. In UF.SIP, the index type of the Σ-type is a
universe. But the results hold for any index type whatsoever, if they
are slightly modified to replace some equivalences by identities. In
particular we don't use univalence (or function or propositional
extensionality) here, which the file UF.SIP does.

we consider Σ-types of the form Σ x ꞉ X , S x. We think of s : S x as
structure on the point x : X, so that S x is the type of all
structures on x, and Σ x ꞉ X , S x is the type of structured points.

Conventions.

* x, y range over X.
* σ, τ range over Σ S.
* s, t range over S x.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.SigmaIdentity 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.Yoneda

module Σ-identity where

\end{code}

Underlying point and structure of a structured point.

\begin{code}

module _ {X : 𝓤 ̇ } {S : X → 𝓥 ̇ } where

⟨_⟩ : Σ S → X
⟨_⟩ = pr₁

structure : (σ : Σ S) → S ⟨ σ ⟩
structure = pr₂

\end{code}

The canonical map from an identification of structures on the same
point to a generalized identification ι with reflexivity data ρ of
structured points with the same underlying point:

\begin{code}

canonical-map : (ι : (σ τ : Σ S) → ⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓦 ̇ )
(ρ : (σ : Σ S) → ι σ σ refl)
{x : X}
(s t : S x)
→ s ＝ t → ι (x , s) (x , t) refl
canonical-map ι ρ {x} s s refl = ρ (x , s)

\end{code}

The type of Sigma notions of identity, ranged over by δ = (ι , ρ , θ).

\begin{code}

SNI : {X : 𝓤 ̇ } → (X → 𝓥 ̇ ) → (𝓦 : Universe) → 𝓤 ⊔ 𝓥 ⊔ (𝓦 ⁺) ̇
SNI {𝓤} {𝓥} {X} S 𝓦 =
Σ ι ꞉ ((σ τ : Σ S) → (⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓦 ̇ ))
, Σ ρ ꞉ ((σ : Σ S) → ι σ σ refl)
, ({x : X} (s t : S x) → is-equiv (canonical-map ι ρ s t))

module _ {X : 𝓤 ̇ } {S : X → 𝓥 ̇ } where

structure-preserving : SNI S 𝓦
→ (σ τ : Σ S) → ⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓦 ̇
structure-preserving (ι , ρ , θ) = ι

_≃[_]_ : Σ S → SNI S 𝓦 → Σ S → 𝓤 ⊔ 𝓦 ̇
σ ≃[ δ ] τ = Σ p ꞉ (⟨ σ ⟩ ＝ ⟨ τ ⟩) , structure-preserving δ σ τ p

structure-preservation-lemma :
(δ : SNI S 𝓦)
(σ τ : Σ S)
(p : ⟨ σ ⟩ ＝ ⟨ τ ⟩)
→ (transport S p (structure σ) ＝ structure τ) ≃ structure-preserving δ σ τ p
structure-preservation-lemma (ι , ρ , θ) (x , s) (x , t) (refl {x}) = γ
where
γ : (s ＝ t) ≃ ι (x , s) (x , t) refl
γ = (canonical-map ι ρ s t , θ s t)

module _ (δ@(ι , ρ , θ) : SNI S 𝓦) where

characterization-of-＝ : (σ τ : Σ S) → (σ ＝ τ) ≃ (σ ≃[ δ ] τ)
characterization-of-＝ σ τ =
(σ ＝ τ)                                                            ≃⟨ i ⟩
(Σ p ꞉ ⟨ σ ⟩ ＝ ⟨ τ ⟩ , transport S p (structure σ) ＝ structure τ) ≃⟨ ii ⟩
(Σ p ꞉ ⟨ σ ⟩ ＝ ⟨ τ ⟩ , structure-preserving δ σ τ p)               ≃⟨ iii ⟩
(σ ≃[ δ ] τ)                                                        ■
where
i   = Σ-＝-≃
ii  = Σ-cong (structure-preservation-lemma δ σ τ)
iii = ≃-refl _

＝-to-≃[] : (σ τ : Σ S) → (σ ＝ τ) → (σ ≃[ δ ] τ)
＝-to-≃[] σ σ refl = refl , ρ σ

characterization-of-characterization-of-＝ :
(σ τ : Σ S) → ⌜ characterization-of-＝ σ τ ⌝ ∼ ＝-to-≃[] σ τ
characterization-of-characterization-of-＝ σ σ refl = refl

＝-to-≃[]-is-equiv : (σ τ : Σ S) → is-equiv (＝-to-≃[] σ τ)
＝-to-≃[]-is-equiv σ τ = equiv-closed-under-∼'
(⌜⌝-is-equiv (characterization-of-＝ σ τ))
(characterization-of-characterization-of-＝ σ τ)

module _ (ι : (σ τ : Σ S) → ⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓦 ̇ )
(ρ : (σ : Σ S) → ι σ σ refl)
{x : X}
where

private
c = canonical-map ι ρ

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

when-canonical-map-is-equiv : ((s t : S x) → is-equiv (c s t))
↔ ((s : S x) → ∃! t ꞉ S x , ι (x , s) (x , t) refl)
when-canonical-map-is-equiv = (λ e s → Yoneda-Theorem-back  s (c s) (e s)) ,
(λ φ s → Yoneda-Theorem-forth s (c s) (φ s))
\end{code}

The canonical map is an equivalence if (and only) if we have some
equivalence.

\begin{code}

canonical-map-equiv-criterion :
((s t : S x) → (s ＝ t) ≃ ι (x , s) (x , t) refl)
→ (s t : S x) → is-equiv (c s t)
canonical-map-equiv-criterion φ s = fiberwise-equiv-criterion'
(λ t → ι (x , s) (x , t) refl)
s (φ s) (c s)
\end{code}

But a retraction suffices for the canonical map to be an equivalence.

\begin{code}

canonical-map-equiv-criterion' :
((s t : S x) → ι (x , s) (x , t) refl ◁ (s ＝ t))
→ (s t : S x) → is-equiv (c s t)
canonical-map-equiv-criterion' φ s = fiberwise-equiv-criterion
(λ t → ι (x , s) (x , t) refl)
s (φ s) (c s)
\end{code}

TODO. The type SNI X 𝓥 should be contractible, with the
following center of contraction, using univalence. Notice that we are
currently not using univalence (or even function or propositional
extensionality) in this file.

\begin{code}

canonical-SNI : {X : 𝓤 ̇ } (S : X → 𝓥 ̇ ) → SNI S 𝓥
canonical-SNI {𝓤} {𝓥} {X} S = ι , ρ , canonical-map-is-equiv
where
ι : (σ τ : Σ S) → (⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓥 ̇ )
ι (x , s) (y , t) p = transport S p s ＝ t

ρ : (σ : Σ S) → ι σ σ refl
ρ (x , s) = refl

canonical-map-is-equiv : {x : X} (s t : S x) → is-equiv (canonical-map ι ρ s t)
canonical-map-is-equiv {x} s t = (canonical-map⁻¹ , η) ,
(canonical-map⁻¹ , ε)
where
canonical-map⁻¹ : ι (x , s) (x , t) refl → s ＝ t
canonical-map⁻¹ refl = refl

η : canonical-map ι ρ s t ∘ canonical-map⁻¹ ∼ id
η refl = refl

ε : canonical-map⁻¹ ∘ canonical-map ι ρ s t ∼ id
ε refl = refl

module Σ-identity-with-axioms where

open Σ-identity

module _ {X : 𝓤 ̇ }
{S : X → 𝓥 ̇ }
(axioms : (x : X) → S x → 𝓦 ̇ )
where

[_] : (Σ x ꞉ X , Σ s ꞉ S x , axioms x s) → Σ S
[ x , s , _ ] = (x , s)

⟪_⟫ : (Σ x ꞉ X , Σ s ꞉ S x , axioms x s) → X
⟪ X , _ , _ ⟫ = X

module _ (axioms-are-prop : (x : X) (s : S x) → is-prop (axioms x s)) where

→ SNI (λ x → Σ s ꞉ S x , axioms x s) 𝓣
add-axioms {𝓣} (ι , ρ , θ) = ι' , ρ' , θ'
where
S' : X → 𝓥 ⊔ 𝓦  ̇
S' x = Σ s ꞉ S x , axioms x s

ι' : (σ τ : Σ S') → ⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓣 ̇
ι' σ τ = ι [ σ ] [ τ ]

ρ' : (σ : Σ S') → ι' σ σ refl
ρ' σ = ρ [ σ ]

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

π-is-embedding : is-embedding π
π-is-embedding = pr₁-is-embedding (axioms-are-prop x)

k : {s' t' : S' x} → is-equiv (ap π {s'} {t'})
k {s'} {t'} = embedding-gives-embedding' π π-is-embedding 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

\end{code}

As expected, the axioms don't contribute to the characterization of
equality.

\begin{code}

characterization-of-＝-with-axioms : (δ : SNI S 𝓣)
→ (σ τ : Σ x ꞉ X , Σ s ꞉ S x , axioms x s)
→ (σ ＝ τ) ≃ ([ σ ] ≃[ δ ] [ τ ])
characterization-of-＝-with-axioms δ = characterization-of-＝ (add-axioms δ)

\end{code}

We now put together two structures on the same type of points.

\begin{code}

module Σ-identity-join where

technical-lemma :
{X : 𝓤 ̇ } {σ : X → X → 𝓥 ̇ }
{Y : 𝓦 ̇ } {τ : Y → Y → 𝓣 ̇ }
(f : (x₀ x₁ : X) → x₀ ＝ x₁ → σ x₀ x₁)
(g : (y₀ y₁ : Y) → y₀ ＝ y₁ → τ 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} {σ} {Y} {τ} f g i j (x₀ , y₀) = γ
where
module _ ((x₁ , y₁) : X × Y) where
r : (x₀ , y₀) ＝ (x₁ , y₁) → σ x₀ x₁ × τ y₀ y₁
r p = f x₀ x₁ (ap pr₁ p) , g y₀ y₁ (ap pr₂ p)

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

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

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

η : (c : σ x₀ x₁ × τ 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 Σ-identity

module _ {X : 𝓤 ̇ }
{S₀ : X → 𝓥₀ ̇ }
{S₁ : X → 𝓥₁ ̇ }
where

⟪_⟫ : (Σ x ꞉ X , S₀ x × S₁ x) → X
⟪ x , s₀ , s₁ ⟫ = x

[_]₀ : (Σ x ꞉ X , S₀ x × S₁ x) → Σ S₀
[ x , s₀ , s₁ ]₀ = (x , s₀)

[_]₁ : (Σ x ꞉ X , S₀ x × S₁ x) → Σ S₁
[ x , s₀ , s₁ ]₁ = (x , s₁)

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

ι : (σ τ : Σ S) → ⟨ σ ⟩ ＝ ⟨ τ ⟩ → 𝓦₀ ⊔ 𝓦₁ ̇
ι σ τ e = ι₀ [ σ ]₀ [ τ ]₀ e  ×  ι₁ [ σ ]₁ [ τ ]₁ e

ρ : (σ : Σ S) → ι σ σ refl
ρ σ = (ρ₀ [ σ ]₀ , ρ₁ [ σ ]₁)

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

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

_≃⟦_,_⟧_ : (Σ x ꞉ X , S₀ x × S₁ x)
→ SNI S₀ 𝓦₀
→ SNI S₁ 𝓦₁
→ (Σ x ꞉ X , S₀ x × S₁ x)
→ 𝓤 ⊔ 𝓦₀ ⊔ 𝓦₁ ̇
σ ≃⟦ δ₀ , δ₁ ⟧ τ = Σ p ꞉ (⟪ σ ⟫ ＝ ⟪ τ ⟫)
, structure-preserving δ₀ [ σ ]₀ [ τ ]₀ p
× structure-preserving δ₁ [ σ ]₁ [ τ ]₁ p

characterization-of-join-＝ : (δ₀ : SNI S₀ 𝓦₀)
(δ₁ : SNI S₁ 𝓦₁)
(σ τ : Σ x ꞉ X , S₀ x × S₁ x)
→ (σ ＝ τ) ≃ (σ ≃⟦ δ₀ , δ₁ ⟧ τ)
characterization-of-join-＝ δ₀ δ₁ = characterization-of-＝ (join δ₀ δ₁)

\end{code}