\begin{code} {-# OPTIONS --safe --without-K #-} module UF.Retracts-FunExt where open import MLTT.Spartan open import UF.Base open import UF.Retracts open import UF.FunExt retract-variance : ∀ {𝓣} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {X' : 𝓦 ̇ } {Y' : 𝓣 ̇ } → funext 𝓤 𝓣 → retract X of X' → retract Y' of Y → retract (X → Y') of (X' → Y) retract-variance {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} {X'} {Y'} fe (rx , sx , rsx) (ry , sy , rsy) = γ where r : (X' → Y) → X → Y' r f x = ry (f (sx x)) s : (X → Y') → X' → Y s f' x' = sy (f' (rx x')) rs' : (f' : X → Y') (x : X) → ry (sy (f' (rx (sx x)))) ＝ f' x rs' f' x = rsy (f' (rx (sx x))) ∙ ap f' (rsx x) rs : (f' : X → Y') → r (s f') ＝ f' rs f' = dfunext fe (rs' f') γ : retract (X → Y') of (X' → Y) γ = (r , s , rs) retract-contravariance : funext 𝓤 𝓦 → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Y' : 𝓦 ̇ } → retract Y' of Y → retract (X → Y') of (X → Y) retract-contravariance fe = retract-variance fe identity-retraction retract-covariance : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {X' : 𝓦 ̇ } → funext 𝓤 𝓥 → retract X of X' → retract (X → Y) of (X' → Y) retract-covariance fe rx = retract-variance fe rx identity-retraction codomain-is-retract-of-function-space-with-pointed-domain : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X → retract Y of (X → Y) codomain-is-retract-of-function-space-with-pointed-domain x = ((λ f → f x) , ((λ y x → y) , λ y → refl)) retracts-of-closed-under-exponentials : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {B : 𝓦 ̇ } → funext 𝓦 𝓦 → X → retract B of X → retract B of Y → retract B of (X → Y) retracts-of-closed-under-exponentials {𝓤} {𝓥} {𝓦} {X} {Y} {B} fe x rbx rby = ii where i : retract (B → B) of (X → Y) i = retract-variance fe rbx rby ii : retract B of (X → Y) ii = retracts-compose i (codomain-is-retract-of-function-space-with-pointed-domain (pr₁ rbx x)) \end{code} TODO. Several retractions here are actually equivalences. So some code should be generalized and moved to an equivalences module. Similarly, some retracts proved here are also shown as equivalences in other modules, and hence there is some amount of repetition that should be removed. This is the result of (1) merging initially independent developments, and (2) work over many years with uncontrolled growth.