{-

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