```{-# OPTIONS --safe #-}
module Cubical.Functions.FunExtEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Vec.Base
open import Cubical.Data.Vec.NAry
open import Cubical.Data.Nat

open import Cubical.Reflection.StrictEquiv

private
variable
ℓ ℓ₁ ℓ₂ ℓ₃ : Level

-- Function extensionality is an equivalence
module _ {A : Type ℓ} {B : A → I → Type ℓ₁}
{f : (x : A) → B x i0} {g : (x : A) → B x i1} where

funExtEquiv : (∀ x → PathP (B x) (f x) (g x)) ≃ PathP (λ i → ∀ x → B x i) f g
unquoteDef funExtEquiv = defStrictEquiv funExtEquiv funExt funExt⁻

funExtPath : (∀ x → PathP (B x) (f x) (g x)) ≡ PathP (λ i → ∀ x → B x i) f g
funExtPath = ua funExtEquiv

funExtIso : Iso (∀ x → PathP (B x) (f x) (g x)) (PathP (λ i → ∀ x → B x i) f g)
funExtIso = iso funExt funExt⁻ (λ x → refl {x = x}) (λ x → refl {x = x})

-- Function extensionality for binary functions
funExt₂ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
{f : (x : A) → (y : B x) → C x y i0}
{g : (x : A) → (y : B x) → C x y i1}
→ ((x : A) (y : B x) → PathP (C x y) (f x y) (g x y))
→ PathP (λ i → ∀ x y → C x y i) f g
funExt₂ p i x y = p x y i

-- Function extensionality for binary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
{f : (x : A) → (y : B x) → C x y i0}
{g : (x : A) → (y : B x) → C x y i1} where
private
appl₂ : PathP (λ i → ∀ x y → C x y i) f g → ∀ x y → PathP (C x y) (f x y) (g x y)
appl₂ eq x y i = eq i x y

funExt₂Equiv : (∀ x y → PathP (C x y) (f x y) (g x y)) ≃ (PathP (λ i → ∀ x y → C x y i) f g)
unquoteDef funExt₂Equiv = defStrictEquiv funExt₂Equiv funExt₂ appl₂

funExt₂Path : (∀ x y → PathP (C x y) (f x y) (g x y)) ≡ (PathP (λ i → ∀ x y → C x y i) f g)
funExt₂Path = ua funExt₂Equiv

-- Function extensionality for ternary functions
funExt₃ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
{D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
{f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
{g : (x : A) → (y : B x) → (z : C x y) → D x y z i1}
→ ((x : A) (y : B x) (z : C x y) → PathP (D x y z) (f x y z) (g x y z))
→ PathP (λ i → ∀ x y z → D x y z i) f g
funExt₃ p i x y z = p x y z i

-- Function extensionality for ternary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
{D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
{f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
{g : (x : A) → (y : B x) → (z : C x y) → D x y z i1} where
private
appl₃ : PathP (λ i → ∀ x y z → D x y z i) f g → ∀ x y z → PathP (D x y z) (f x y z) (g x y z)
appl₃ eq x y z i = eq i x y z

funExt₃Equiv : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≃ (PathP (λ i → ∀ x y z → D x y z i) f g)
unquoteDef funExt₃Equiv = defStrictEquiv funExt₃Equiv funExt₃ appl₃

funExt₃Path : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≡ (PathP (λ i → ∀ x y z → D x y z i) f g)
funExt₃Path = ua funExt₃Equiv

-- n-ary non-dependent funext
nAryFunExt : {X : Type ℓ} {Y : I → Type ℓ₁} (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
→ ((xs : Vec X n) → PathP Y (fX \$ⁿ xs) (fY \$ⁿ map (λ x → x) xs))
→ PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExt zero fX fY p        = p []
nAryFunExt (suc n) fX fY p i x = nAryFunExt n (fX x) (fY x) (λ xs → p (x ∷ xs)) i

-- n-ary funext⁻
nAryFunExt⁻ : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
→ PathP (λ i → nAryOp n X (Y i)) fX fY
→ ((xs : Vec X n) → PathP Y (fX \$ⁿ xs) (fY \$ⁿ map (λ x → x) xs))
nAryFunExt⁻ zero fX fY p [] = p
nAryFunExt⁻ (suc n) fX fY p (x ∷ xs) = nAryFunExt⁻ n (fX x) (fY x) (λ i → p i x) xs

nAryFunExtEquiv : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
→ ((xs : Vec X n) → PathP Y (fX \$ⁿ xs) (fY \$ⁿ map (λ x → x) xs)) ≃ PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExtEquiv n {X} {Y} fX fY = isoToEquiv (iso (nAryFunExt n fX fY) (nAryFunExt⁻ n fX fY)
(linv n fX fY) (rinv n fX fY))
where
linv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
(p : PathP (λ i → nAryOp n X (Y i)) fX fY)
→ nAryFunExt n fX fY (nAryFunExt⁻ n fX fY p) ≡ p
linv zero fX fY p          = refl
linv (suc n) fX fY p i j x = linv n (fX x) (fY x) (λ k → p k x) i j

rinv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
(p : (xs : Vec X n) → PathP Y (fX \$ⁿ xs) (fY \$ⁿ map (λ x → x) xs))
→ nAryFunExt⁻ n fX fY (nAryFunExt n fX fY p) ≡ p
rinv zero fX fY p i []          = p []
rinv (suc n) fX fY p i (x ∷ xs) = rinv n (fX x) (fY x) (λ ys i → p (x ∷ ys) i) i xs

-- Funext when the domain also depends on the interval

funExtDep : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
{f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
→ ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
→ PathP (λ i → (x : A i) → B i x) f g
funExtDep {A = A} {B} {f} {g} h i x =
comp
(λ k → B i (coei→i A i x k))
(λ k → λ
{ (i = i0) → f (coei→i A i0 x k)
; (i = i1) → g (coei→i A i1 x k)
})
(h (λ j → coei→j A i j x) i)

funExtDep⁻ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
{f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
→ PathP (λ i → (x : A i) → B i x) f g
→ ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
funExtDep⁻ q p i = q i (p i)

funExtDepEquiv : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
{f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
→ ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
≃ PathP (λ i → (x : A i) → B i x) f g
funExtDepEquiv {A = A} {B} {f} {g} = isoToEquiv isom
where
open Iso
isom : Iso _ _
isom .fun = funExtDep
isom .inv = funExtDep⁻
isom .rightInv q m i x =
comp
(λ k → B i (coei→i A i x (k ∨ m)))
(λ k → λ
{ (i = i0) → f (coei→i A i0 x (k ∨ m))
; (i = i1) → g (coei→i A i1 x (k ∨ m))
; (m = i1) → q i x
})
(q i (coei→i A i x m))
isom .leftInv h m p i =
comp
(λ k → B i (lemi→i m k))
(λ k → λ
{ (i = i0) → f (lemi→i m k)
; (i = i1) → g (lemi→i m k)
; (m = i1) → h p i
})
(h (λ j → lemi→j j m) i)
where
lemi→j : ∀ j → coei→j A i j (p i) ≡ p j
lemi→j j =
coei→j (λ k → coei→j A i k (p i) ≡ p k) i j (coei→i A i (p i))

lemi→i : PathP (λ m → lemi→j i m ≡ p i) (coei→i A i (p i)) refl
lemi→i =
sym (coei→i (λ k → coei→j A i k (p i) ≡ p k) i (coei→i A i (p i)))
◁ λ m k → lemi→j i (m ∨ k)

heteroHomotopy≃Homotopy : {A : I → Type ℓ} {B : (i : I) → Type ℓ₁}
{f : A i0 → B i0} {g : A i1 → B i1}
→ ({x₀ : A i0} {x₁ : A i1} → PathP A x₀ x₁ → PathP B (f x₀) (g x₁))
≃ ((x₀ : A i0) → PathP B (f x₀) (g (transport (λ i → A i) x₀)))
heteroHomotopy≃Homotopy {A = A} {B} {f} {g} = isoToEquiv isom
where
open Iso
isom : Iso _ _
isom .fun h x₀ = h (isContrSinglP A x₀ .fst .snd)
isom .inv k {x₀} {x₁} p =
subst (λ fib → PathP B (f x₀) (g (fib .fst))) (isContrSinglP A x₀ .snd (x₁ , p)) (k x₀)
isom .rightInv k = funExt λ x₀ →
cong (λ α → subst (λ fib → PathP B (f x₀) (g (fib .fst))) α (k x₀))
(isProp→isSet isPropSinglP (isContrSinglP A x₀ .fst) _
(isContrSinglP A x₀ .snd (isContrSinglP A x₀ .fst))
refl)
∙ transportRefl (k x₀)
isom .leftInv h j {x₀} {x₁} p =
transp
(λ i → PathP B (f x₀) (g (isContrSinglP A x₀ .snd (x₁ , p) (i ∨ j) .fst)))
j
(h (isContrSinglP A x₀ .snd (x₁ , p) j .snd))
```