Martin Escardo, 13th January 2021.

Interface to code from my MGS 2019 lecture notes.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.Lower-FunExt where

open import MLTT.Spartan
open import UF.Base
open import UF.Equiv
open import UF.FunExt

open import MGS.TypeTopology-Interface

import MGS.Equivalences
import MGS.FunExt-from-Univalence
import MGS.Universe-Lifting

abstract

  lower-DN-funext : ∀ 𝓦 𝓣 → DN-funext (𝓤 ⊔ 𝓦) (𝓥 ⊔ 𝓣) → DN-funext 𝓤 𝓥
  lower-DN-funext {𝓤} {𝓥} 𝓦 𝓣 fe = MGS.Universe-Lifting.lower-dfunext 𝓦 𝓣 𝓤 𝓥 fe

  DN-funext-gives-funext : {𝓤 𝓥 : Universe} → DN-funext 𝓤 𝓥 → funext 𝓤 𝓥
  DN-funext-gives-funext dnfe {X} {A} f g = γ
   where
    h : f ＝ g → f ∼ g
    h = MGS.FunExt-from-Univalence.happly f g

    a : is-equiv h
    a = MGS-equivs-are-equivs h (MGS.FunExt-from-Univalence.dfunext-gives-hfunext dnfe f g)

    b : is-equiv (happly' f g)
    b = equiv-closed-under-∼ h (happly' f g) a (happly'-is-MGS-happly f g)

    c :  MGS.Equivalences.is-equiv (happly' f g)
    c = equivs-are-MGS-equivs (happly' f g) b

    γ : is-equiv (happly' f g)
    γ = MGS-equivs-are-equivs (happly' f g) c

  lower-funext : ∀ 𝓦 𝓣 → funext (𝓤 ⊔ 𝓦) (𝓥 ⊔ 𝓣) → funext 𝓤 𝓥
  lower-funext {𝓤} {𝓥} 𝓦 𝓣 fe = DN-funext-gives-funext
                                   (lower-DN-funext 𝓦 𝓣 (dfunext fe))

  lower-fun-ext : ∀ {𝓦} 𝓣 → funext (𝓤 ⊔ 𝓦) (𝓥 ⊔ 𝓣) → funext 𝓤 𝓥
  lower-fun-ext {𝓤} {𝓥} {𝓦} 𝓣 fe = DN-funext-gives-funext
                                      (lower-DN-funext 𝓦 𝓣 (dfunext fe))

\end{code}