TerminalLarge.agda

module TerminalLarge where
open import 1Lab.Prelude

module
  _
  {ℓ}
  (X : Type ℓ)
  (Y : Type) (f : Y → X)
  (f-term : (Z : Type) (g : Z → X) → is-contr (Σ[ h ∈ (Z → Y) ] f ∘ h ≡ g))
  where

  f-equiv : is-equiv f
  f-equiv .is-eqv x =
    Equiv→is-hlevel 0
      (Σ-ap (Π-contr-eqv (hlevel 0)) (λ _ → ap-equiv (Π-contr-eqv (hlevel 0))) e⁻¹)
      (f-term ⊤ (λ _ → x))