{-# OPTIONS --safe #-}
module Cubical.Foundations.Pointed.FunExt where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Foundations.Pointed.Homotopy
private
  variable
     ℓ' : Level
module _ {A : Pointed } {B : typ A  Type ℓ'} {ptB : B (pt A)} where
  -- pointed function extensionality
  funExt∙P : {f g : Π∙ A B ptB}  f ∙∼P g  f  g
  funExt∙P (h , h∙) i .fst x = h x i
  funExt∙P (h , h∙) i .snd = h∙ i
  -- inverse of pointed function extensionality
  funExt∙P⁻ : {f g : Π∙ A B ptB}  f  g  f ∙∼P g
  funExt∙P⁻ p .fst a i = p i .fst a
  funExt∙P⁻ p .snd i = p i .snd
  -- function extensionality is an isomorphism, PathP version
  funExt∙PIso : (f g : Π∙ A B ptB)  Iso (f ∙∼P g) (f  g)
  Iso.fun (funExt∙PIso f g)  = funExt∙P {f = f} {g = g}
  Iso.inv (funExt∙PIso f g) = funExt∙P⁻ {f = f} {g = g}
  Iso.rightInv (funExt∙PIso f g) p i j = p j
  Iso.leftInv (funExt∙PIso f g) h _ = h
  -- transformed to equivalence
  funExt∙P≃ : (f g : Π∙ A B ptB)  (f ∙∼P g)  (f  g)
  funExt∙P≃ f g = isoToEquiv (funExt∙PIso f g)
  -- funExt∙≃ using the other kind of pointed homotopy
  funExt∙≃ : (f g : Π∙ A B ptB)  (f ∙∼ g)  (f  g)
  funExt∙≃ f g = compEquiv (∙∼≃∙∼P f g) (funExt∙P≃ f g)
  -- standard pointed function extensionality and its inverse
  funExt∙ : {f g : Π∙ A B ptB}  f ∙∼ g  f  g
  funExt∙ {f = f} {g = g} = equivFun (funExt∙≃ f g)
  funExt∙⁻ : {f g : Π∙ A B ptB}  f  g  f ∙∼ g
  funExt∙⁻ {f = f} {g = g} = equivFun (invEquiv (funExt∙≃ f g))