{-

Functions between structures S and T: X ↦ S X → T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Function where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Nat
open import Cubical.Data.Vec

private
  variable
     ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level

-- General function structure

FunctionStructure : (S : Type   Type ℓ₁) (T : Type   Type ℓ₂)
   Type   Type (ℓ-max ℓ₁ ℓ₂)
FunctionStructure S T X = S X  T X

FunctionEquivStr : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
   StrEquiv S ℓ₁'  StrEquiv T ℓ₂'
   StrEquiv (FunctionStructure S T) (ℓ-max ℓ₁ (ℓ-max ℓ₁' ℓ₂'))
FunctionEquivStr {S = S} {T} ι₁ ι₂ (X , f) (Y , g) e =
  {s : S X} {t : S Y}  ι₁ (X , s) (Y , t) e  ι₂ (X , f s) (Y , g t) e

functionUnivalentStr : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
  (ι₁ : StrEquiv S ℓ₁') (θ₁ : UnivalentStr S ι₁)
  (ι₂ : StrEquiv T ℓ₂') (θ₂ : UnivalentStr T ι₂)
   UnivalentStr (FunctionStructure S T) (FunctionEquivStr ι₁ ι₂)
functionUnivalentStr ι₁ θ₁ ι₂ θ₂ e =
  compEquiv
    (equivImplicitΠCod (equivImplicitΠCod (equiv→ (θ₁ e) (θ₂ e))))
    funExtDepEquiv

functionEquivAction : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
   EquivAction S  EquivAction T
   EquivAction (FunctionStructure S T)
functionEquivAction α₁ α₂ e = equiv→ (α₁ e) (α₂ e)

functionTransportStr : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
  (α₁ : EquivAction S) (τ₁ : TransportStr α₁)
  (α₂ : EquivAction T) (τ₂ : TransportStr α₂)
   TransportStr (functionEquivAction α₁ α₂)
functionTransportStr {S = S} α₁ τ₁ α₂ τ₂ e f =
  funExt λ t 
  cong (equivFun (α₂ e)  f) (invTransportStr α₁ τ₁ e t)
   τ₂ e (f (subst⁻ S (ua e) t))

-- Definition of structured equivalence using an action in the domain

FunctionEquivStr+ : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
   EquivAction S  StrEquiv T ℓ₂'
   StrEquiv (FunctionStructure S T) (ℓ-max ℓ₁ ℓ₂')
FunctionEquivStr+ {S = S} {T} α₁ ι₂ (X , f) (Y , g) e =
  (s : S X)  ι₂ (X , f s) (Y , g (equivFun (α₁ e) s)) e

functionUnivalentStr+ : {S : Type   Type ℓ₁} {T : Type   Type ℓ₂}
  (α₁ : EquivAction S) (τ₁ : TransportStr α₁)
  (ι₂ : StrEquiv T ℓ₂') (θ₂ : UnivalentStr T ι₂)
   UnivalentStr (FunctionStructure S T) (FunctionEquivStr+ α₁ ι₂)
functionUnivalentStr+ {S = S} {T} α₁ τ₁ ι₂ θ₂ {X , f} {Y , g} e =
  compEquiv
    (compEquiv
      (equivΠCod λ s 
        compEquiv
          (θ₂ e)
          (pathToEquiv (cong (PathP  i  T (ua e i)) (f s)  g) (τ₁ e s))))
      (invEquiv heteroHomotopy≃Homotopy))
    funExtDepEquiv