{-

In this file we apply the cubical machinery to Martin Hötzel-Escardó's
structure identity principle:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.SIP where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv')
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma

open import Cubical.Foundations.Structure public

private
variable
ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level
S : Type ℓ₁ → Type ℓ₂

-- Note that for any equivalence (f , e) : X ≃ Y the type  ι (X , s) (Y , t) (f , e) need not to be
-- a proposition. Indeed this type should correspond to the ways s and t can be identified
-- as S-structures. This we call a standard notion of structure or SNS.
-- We will use a different definition, but the two definitions are interchangeable.
SNS : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
SNS {ℓ₁} S ι = ∀ {X : Type ℓ₁} (s t : S X) → ι (X , s) (X , t) (idEquiv X) ≃ (s ≡ t)

-- We introduce the notation for structure preserving equivalences a
-- bit differently, but this definition doesn't actually change from
-- Escardó's notes.
_≃[_]_ : (A : TypeWithStr ℓ₁ S) (ι : StrEquiv S ℓ₂) (B : TypeWithStr ℓ₁ S) → Type (ℓ-max ℓ₁ ℓ₂)
A ≃[ ι ] B = Σ[ e ∈ typ A ≃ typ B ] (ι A B e)

-- The following PathP version of SNS is a bit easier to work with
-- for the proof of the SIP
UnivalentStr : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
UnivalentStr {ℓ₁} S ι =
{A B : TypeWithStr ℓ₁ S} (e : typ A ≃ typ B)
→ ι A B e ≃ PathP (λ i → S (ua e i)) (str A) (str B)

-- A quick sanity-check that our definition is interchangeable with
-- Escardó's. The direction SNS→UnivalentStr corresponds more or less
-- to a dependent EquivJ formulation of Escardó's homomorphism-lemma.
UnivalentStr→SNS : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃)
→ UnivalentStr S ι → SNS S ι
UnivalentStr→SNS S ι θ {X = X} s t =
ι (X , s) (X , t) (idEquiv X)
≃⟨ θ (idEquiv X) ⟩
PathP (λ i → S (ua (idEquiv X) i)) s t
≃⟨ transportEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = X} j i)) s t) ⟩
s ≡ t
■

SNS→UnivalentStr : (ι : StrEquiv S ℓ₃) → SNS S ι → UnivalentStr S ι
SNS→UnivalentStr {S = S} ι θ {A = A} {B = B} e = EquivJ P C e (str A) (str B)
where
Y = typ B

P : (X : Type _) → X ≃ Y → Type _
P X e' = (s : S X) (t : S Y) → ι (X , s) (Y , t) e' ≃ PathP (λ i → S (ua e' i)) s t

C : (s t : S Y) → ι (Y , s) (Y , t) (idEquiv Y) ≃ PathP (λ i → S (ua (idEquiv Y) i)) s t
C s t =
ι (Y , s) (Y , t) (idEquiv Y)
≃⟨ θ s t ⟩
s ≡ t
≃⟨ transportEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = Y} (~ j) i)) s t) ⟩
PathP (λ i → S (ua (idEquiv Y) i)) s t
■

TransportStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S) → Type (ℓ-max (ℓ-suc ℓ) ℓ₁)
TransportStr {ℓ} {S = S} α =
{X Y : Type ℓ} (e : X ≃ Y) (s : S X) → equivFun (α e) s ≡ subst S (ua e) s

TransportStr→UnivalentStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S)
→ TransportStr α → UnivalentStr S (EquivAction→StrEquiv α)
TransportStr→UnivalentStr {S = S} α τ {X , s} {Y , t} e =
equivFun (α e) s ≡ t
≃⟨ pathToEquiv (cong (_≡ t) (τ e s)) ⟩
subst S (ua e) s ≡ t
≃⟨ invEquiv (PathP≃Path _ _ _) ⟩
PathP (λ i → S (ua e i)) s t
■

UnivalentStr→TransportStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S)
→ UnivalentStr S (EquivAction→StrEquiv α) → TransportStr α
UnivalentStr→TransportStr {S = S} α θ e s =
invEq (θ e) (transport-filler (cong S (ua e)) s)

invTransportStr : {S : Type ℓ → Type ℓ₂} (α : EquivAction S) (τ : TransportStr α)
{X Y : Type ℓ} (e : X ≃ Y) (t : S Y) → invEq (α e) t ≡ subst⁻ S (ua e) t
invTransportStr {S = S} α τ e t =
sym (transport⁻Transport (cong S (ua e)) (invEq (α e) t))
∙∙ sym (cong (subst⁻ S (ua e)) (τ e (invEq (α e) t)))
∙∙ cong (subst⁻ S (ua e)) (retEq (α e) t)

--- We can now define an invertible function
---
---    sip : A ≃[ ι ] B → A ≡ B

module _ {S : Type ℓ₁ → Type ℓ₂} {ι : StrEquiv S ℓ₃}
(θ : UnivalentStr S ι) (A B : TypeWithStr ℓ₁ S)
where

sip : A ≃[ ι ] B → A ≡ B
sip (e , p) i = ua e i , θ e .fst p i

SIP : A ≃[ ι ] B ≃ (A ≡ B)
SIP =
sip , isoToIsEquiv (compIso (Σ-cong-iso (invIso univalenceIso) (equivToIso ∘ θ)) ΣPathIsoPathΣ)

sip⁻ : A ≡ B → A ≃[ ι ] B
sip⁻ = invEq SIP