Martin Escardo, 20th August 2018

We consider type and subtype classifiers, and discuss an obvious
generalization.

 * (Ξ£ X κž‰ 𝓀 Μ‡ , X β†’ Y) ≃ (Y β†’ 𝓀 Μ‡ )
 * (Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y) ≃ (Y β†’ Ξ© 𝓀)

\begin{code}

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

module UF.Classifiers-Old where

open import MLTT.Spartan
open import UF.Subsingletons
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Equiv-FunExt
open import UF.Base
open import UF.Univalence
open import UF.UA-FunExt
open import UF.FunExt
open import UF.Embeddings
open import UF.SubtypeClassifier

module type-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 Ο‡ : (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y))  β†’ (Y β†’ 𝓀 Μ‡ )
 Ο‡ (X , f) = fiber f

 T : (Y β†’ 𝓀 Μ‡ ) β†’ Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)
 T A = Ξ£ A , pr₁

 Ο‡T : (A : Y β†’ 𝓀 Μ‡ ) β†’ Ο‡ (T A) ＝ A
 Ο‡T A = dfunext fe' Ξ³
  where
   f : βˆ€ y β†’ (Ξ£ Οƒ κž‰ Ξ£ A , pr₁ Οƒ ＝ y) β†’ A y
   f y ((.y , a) , refl) = a
   g : βˆ€ y β†’ A y β†’ Ξ£ Οƒ κž‰ Ξ£ A , pr₁ Οƒ ＝ y
   g y a = (y , a) , refl
   fg : βˆ€ y a β†’ f y (g y a) ＝ a
   fg y a = refl
   gf : βˆ€ y Οƒ β†’ g y (f y Οƒ) ＝ Οƒ
   gf y ((.y , a) , refl) = refl
   Ξ³ : βˆ€ y β†’ (Ξ£ Οƒ κž‰ Ξ£ A , pr₁ Οƒ ＝ y) ＝ A y
   Ξ³ y = eqtoid ua _ _ (f y , ((g y , fg y) , (g y , gf y)))

 transport-map : {X X' Y : 𝓀 Μ‡ } (e : X ≃ X') (g : X β†’ Y)
               β†’ transport (Ξ» - β†’ - β†’ Y) (eqtoid ua X X' e) g
               ＝ g ∘ eqtofun (≃-sym e)

 transport-map {X} {X'} {Y} e g = Ο„ (eqtoid ua X X' e) refl
  where
   Ο„ : (p : X ＝ X')
     β†’ p ＝ eqtoid ua X X' e
     β†’ transport (Ξ» - β†’ - β†’ Y) p g ＝ g ∘ eqtofun (≃-sym e)
   Ο„ refl q = ap (Ξ» h β†’ g ∘ h) s
    where
     r : idtoeq X X refl ＝ e
     r = idtoeq X X refl              ＝⟨ ap (idtoeq X X) q ⟩
         idtoeq X X (eqtoid ua X X e) ＝⟨ idtoeq-eqtoid ua X X e ⟩
         e                            ∎
     s : id ＝ eqtofun (≃-sym e)
     s = ap (Ξ» - β†’ eqtofun (≃-sym -)) r

 TΟ‡ : (Οƒ : Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) β†’ T (Ο‡ Οƒ) ＝ Οƒ
 TΟ‡ (X , f) = to-Ξ£-＝ (eqtoid ua _ _ (total-fiber-is-domain f) ,
                       transport-map (total-fiber-is-domain f) pr₁)

 Ο‡-is-equivalence : is-equiv Ο‡
 χ-is-equivalence = (T , χT) , (T , Tχ)

 classification-equivalence : (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) ≃ (Y β†’ 𝓀 Μ‡ )
 classification-equivalence = Ο‡ , Ο‡-is-equivalence


module subtype-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 fe : funext 𝓀 𝓀
 fe = univalence-gives-funext ua

 Ο‡ : (Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y)  β†’ (Y β†’ Ξ© 𝓀)
 Ο‡ (X , f , i) y = fiber f y , i y

 T : (Y β†’ Ξ© 𝓀) β†’ Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y
 T P = (Ξ£ y κž‰ Y , P y holds) , pr₁ , pr₁-is-embedding (Ξ» y β†’ holds-is-prop (P y))

 Ο‡T : (P : Y β†’ Ξ© 𝓀) β†’ Ο‡ (T P) ＝ P
 Ο‡T P = dfunext fe' Ξ³
  where
   f : βˆ€ y β†’ Ο‡ (T P) y holds β†’ P y holds
   f y ((.y , h) , refl) = h
   g : βˆ€ y β†’ P y holds β†’ Ο‡ (T P) y holds
   g y h = (y , h) , refl
   Ξ³ : (y : Y) β†’ Ο‡ (T P) y ＝ P y
   Ξ³ y = Ξ©-ext-from-univalence ua (f y) (g y)

 transport-embedding : {X X' Y : 𝓀 Μ‡ } (e : X ≃ X') (g : X β†’ Y) (i : is-embedding g)
                    β†’ transport (Ξ» - β†’ - β†ͺ Y) (eqtoid ua X X' e) (g , i)
                    ＝ g ∘ eqtofun (≃-sym e) , ∘-is-embedding
                                                 (equivs-are-embeddings (eqtofun (≃-sym e))
                                                                        (eqtofun- (≃-sym e))) i
 transport-embedding {X} {X'} {Y} e g i = Ο„ (eqtoid ua X X' e) refl
  where
   Ο„ : (p : X ＝ X')
     β†’ p ＝ eqtoid ua X X' e
     β†’ transport (Ξ» - β†’ - β†ͺ Y) p (g , i)
     ＝ g ∘ eqtofun (≃-sym e) , ∘-is-embedding
                                  (equivs-are-embeddings (eqtofun (≃-sym e))
                                                         (eqtofun- (≃-sym e))) i
   Ο„ refl q = to-Ξ£-＝ (ap (Ξ» h β†’ g ∘ h) s ,
                      being-embedding-is-prop fe (g ∘ eqtofun (≃-sym e)) _ _)
    where
     r : idtoeq X X refl ＝ e
     r = ap (idtoeq X X) q βˆ™ idtoeq-eqtoid ua X X e
     s : id ＝ eqtofun (≃-sym e)
     s = ap (Ξ» - β†’ eqtofun (≃-sym -)) r

 TΟ‡ : (Οƒ : Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y) β†’ T (Ο‡ Οƒ) ＝ Οƒ
 TΟ‡ (X , f , i) = to-Ξ£-＝ (eqtoid ua _ _ (total-fiber-is-domain f) ,
                          (transport-embedding (total-fiber-is-domain f) pr₁ (pr₁-is-embedding i)
                         βˆ™ to-Ξ£-＝' (being-embedding-is-prop fe f _ _)))

 Ο‡-is-equivalence : is-equiv Ο‡
 χ-is-equivalence = (T , χT) , (T , Tχ)

 classification-equivalence : (Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y) ≃ (Y β†’ Ξ© 𝓀)
 classification-equivalence = Ο‡ , Ο‡-is-equivalence

\end{code}

TODO. Consider a property "green" of types, and call a map green if
its fibers are all green. Then the maps of Y into green types should
correspond to the green maps X β†’ Y. This generalizes the above
situation. In particular, the case green = contractible is of interest
and describes a previously known situation. Another example is that
surjections X β†’ Y are in bijection with families
Y β†’ Ξ£ (Z : 𝓀 Μ‡ ) β†’ βˆ₯ Z βˆ₯), that is, families of inhabited types. It is
not necessary that "green" is proposition valued. It can be universe
valued in general. And then of course retractions X β†’ Y are in
bijections with families of pointed types.

Tom de Jong, September 2019. I implement the above TODO.

(There is an alternative solution at
https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/)

Fix type universes 𝓀 and π“₯ and a type Y : 𝓀 Μ‡. Consider a property green : 𝓀 β†’ π“₯.
If X : 𝓀 Μ‡ and f : X β†’ Y, then we say that f is a green map if all of its fibers
are green.

The general theorem says that type of green maps to Y is equivalent to the type
of green types: Green-map ≃ (Y β†’ Green).

The examples are obtained by specialising to a specific property green:

 * Every type and map is green.
   (Ξ£ X κž‰ 𝓀 Μ‡ , X β†’ Y) ≃ (Y β†’ 𝓀 Μ‡ )

 * A type is green exactly if it is a subsingleton.
   Then a map is green exactly if it is an embedding.
   (Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y) ≃ (Y β†’ Ξ© 𝓀)

 * A type is green exactly if it is inhabited.
   Then a map is green exactly if it is a surjection.
   (Ξ£ X κž‰ 𝓀 Μ‡ , (Ξ£ f κž‰ X β†’ Y , is-surjection f )) ≃ (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , βˆ₯ X βˆ₯))

 * A type is green exactly if it is pointed.
   Then a map is green exactly if it is a retraction.
   (Ξ£ X κž‰ 𝓀 Μ‡ , Y ◁ X) ≃ (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , X))

\begin{code}

eqtoid-comp : (ua : is-univalent 𝓀) {X Y Z : 𝓀 Μ‡ } (f : X ≃ Y) (g : Y ≃ Z)
            β†’ (eqtoid ua X Y f) βˆ™ (eqtoid ua Y Z g) ＝ eqtoid ua X Z (f ● g)
eqtoid-comp {𝓀} ua {X} {Y} {Z} f =
 JEq ua Y (Ξ» Z g β†’ eqtoid ua X Y f βˆ™ eqtoid ua Y Z g ＝ eqtoid ua X Z (f ● g)) Ξ³ Z
  where
   fe : funext 𝓀 𝓀
   fe = univalence-gives-funext ua
   h : f ＝ f ● ≃-refl Y
   h = (≃-refl-right' fe fe fe f)⁻¹

   Ξ³ = eqtoid ua X Y f βˆ™ eqtoid ua Y Y (≃-refl Y) ＝⟨ ap (Ξ» - β†’ eqtoid ua X Y f βˆ™ -) (eqtoid-refl ua Y) ⟩
       eqtoid ua X Y f                            ＝⟨ ap (Ξ» - β†’ eqtoid ua X Y -) h ⟩
       eqtoid ua X Y (f ● ≃-refl Y)               ∎

module general-classifier
        {𝓀 π“₯ : Universe}
        (fe : funext 𝓀 π“₯)
        (fe' : funext 𝓀 (𝓀 ⁺ βŠ” π“₯))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
        (green : 𝓀 Μ‡ β†’ π“₯ Μ‡ )
       where

 green-map : {X : 𝓀 Μ‡ } β†’ (X β†’ Y) β†’ 𝓀 βŠ” π“₯ Μ‡
 green-map f = (y : Y) β†’ green (fiber f y)

 Green : 𝓀 ⁺ βŠ” π“₯ Μ‡
 Green = Ξ£ X κž‰ 𝓀 Μ‡ , green X

 Green-map : 𝓀 ⁺ βŠ” π“₯ Μ‡
 Green-map = Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , green-map f

 Ο‡ : Green-map  β†’ (Y β†’ Green)
 Ο‡ (X , f , g) y = (fiber f y) , (g y)

 fiber-equiv-＝ : (A : Y β†’ Green) (y : Y) β†’ pr₁ (A y) ＝ fiber pr₁ y
 fiber-equiv-＝ A y =
  (eqtoid ua (fiber pr₁ y) (pr₁ (A y)) (pr₁-fiber-equiv {𝓀} {𝓀} {Y} {pr₁ ∘ A} y)) ⁻¹

 T : (Y β†’ Green) β†’ Green-map
 T A = Ξ£ (pr₁ ∘ A) , pr₁ , g
  where
   g : green-map pr₁
   g y = transport green (fiber-equiv-＝ A y) (prβ‚‚ (A y))

 Ο‡T : (A : Y β†’ Green) β†’ Ο‡ (T A) ＝ A
 Ο‡T A = dfunext fe' Ξ³
  where
   Ξ³ : (y : Y) β†’ Ο‡ (T A) y ＝ A y
   γ y = to-Σ-＝ ((a ⁻¹) , b)
    where
     a : pr₁ (A y) ＝ pr₁ (Ο‡ (T A) y)
     a = fiber-equiv-＝ A y
     b = transport green (a ⁻¹) (prβ‚‚ (Ο‡ (T A) y))               ＝⟨ refl ⟩
         transport green (a ⁻¹) (transport green a (prβ‚‚ (A y))) ＝⟨ i ⟩
         transport green (a βˆ™ a ⁻¹) (prβ‚‚ (A y))                 ＝⟨ ii ⟩
         transport green refl (prβ‚‚ (A y))                       ＝⟨ refl ⟩
         prβ‚‚ (A y)                                              ∎
      where
       i  = (transport-βˆ™ green a (a ⁻¹)) ⁻¹
       ii = ap (Ξ» - β†’ transport green - (prβ‚‚ (A y))) (trans-sym' a)

 green-maps-are-closed-under-precomp-with-equivs : {X X' : 𝓀 Μ‡ } (e : X' ≃ X)
                                                   {f : X β†’ Y}
                                                 β†’ green-map f
                                                 β†’ green-map (f ∘ eqtofun e)
 green-maps-are-closed-under-precomp-with-equivs e {f} g y =
  transport green p (g y)
   where
    p : fiber f y ＝ fiber (f ∘ eqtofun e) y
    p = (eqtoid ua _ _ (precomposition-with-equiv-does-not-change-fibers e f y)) ⁻¹

 precomp-with-≃-refl-green-map : {X : 𝓀 Μ‡ } (f : X β†’ Y) (g : green-map f)
                           β†’ green-maps-are-closed-under-precomp-with-equivs
                              (≃-refl X) g
                             ＝ g
 precomp-with-≃-refl-green-map {X} f g = dfunext fe Ξ³
  where
   Ξ³ : (y : Y) β†’ green-maps-are-closed-under-precomp-with-equivs (≃-refl X) g y ＝ g y
   Ξ³ y = green-maps-are-closed-under-precomp-with-equivs (≃-refl X) g y         ＝⟨ refl ⟩
         transport green ((eqtoid ua _ _ (≃-refl (fiber f y))) ⁻¹) (g y)        ＝⟨ i ⟩
         g y                                                                    ∎
    where
     i = ap (Ξ» - β†’ transport green (- ⁻¹) (g y)) (eqtoid-refl ua (fiber f y))

 transport-green-map-eqtoid : {X X' : 𝓀 Μ‡ } (e : X' ≃ X) (f : X β†’ Y)
                              (g : green-map f)
                            β†’ transport (Ξ» - β†’ Ξ£ h κž‰ (- β†’ Y) , green-map h)
                               ((eqtoid ua X' X e) ⁻¹) (f , g)
                              ＝
                              f ∘ (eqtofun e) ,
                               green-maps-are-closed-under-precomp-with-equivs e g
 transport-green-map-eqtoid {X} {X'} = JEq ua X' E Ξ³ X
  where
   B : 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
   B Z = Ξ£ h κž‰ (Z β†’ Y) , green-map h
   E : (Z : 𝓀 Μ‡ ) β†’ X' ≃ Z β†’ 𝓀 βŠ” π“₯ Μ‡
   E Z e = (f : Z β†’ Y) β†’ (g : green-map f)
         β†’ transport B ((eqtoid ua X' Z e) ⁻¹) (f , g)
           ＝ f ∘ (eqtofun e) , green-maps-are-closed-under-precomp-with-equivs e g
   Ξ³ : E X' (≃-refl X')
   Ξ³ f g = transport B ((eqtoid ua X' X' (≃-refl X')) ⁻¹) (f , g)            ＝⟨ i ⟩
           f , g                                                             ＝⟨ ii ⟩
           f , green-maps-are-closed-under-precomp-with-equivs (≃-refl X') g ∎
    where
     i  = ap (Ξ» - β†’ transport B (- ⁻¹) (f , g)) (eqtoid-refl ua X')
     ii = to-Ξ£-＝ (refl , ((precomp-with-≃-refl-green-map f g) ⁻¹))

 TΟ‡ : (f : Green-map) β†’ T (Ο‡ f) ＝ f
 TΟ‡ (X , f , g) = to-Ξ£-＝ (a , (to-Ξ£-＝ (b , c)))
  where
   X' : 𝓀 Μ‡
   X' = pr₁ (T (Ο‡ (X , f , g)))
   f' : X' β†’ Y
   f' = pr₁ (prβ‚‚ (T (Ο‡ (X , f , g))))
   g' : green-map f'
   g' = prβ‚‚ (prβ‚‚ (T (Ο‡ (X , f , g))))
   e : X ≃ X'
   e = domain-is-total-fiber f
   a : X' ＝ X
   a = (eqtoid ua X X' e) ⁻¹
   B : 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ Μ‡
   B Z = Ξ£ h κž‰ (Z β†’ Y), green-map h
   t : transport B a (f' , g') ＝
       (f' ∘ eqtofun e) , (green-maps-are-closed-under-precomp-with-equivs e g')
   t = transport-green-map-eqtoid e f' g'
   t₁ : pr₁ (transport B a (f' , g')) ＝ f' ∘ eqtofun e
   t₁ = pr₁ (from-Ξ£-＝ t)
   tβ‚‚ : transport green-map t₁ (prβ‚‚ (transport B a (f' , g'))) ＝
        green-maps-are-closed-under-precomp-with-equivs e g'
   tβ‚‚ = prβ‚‚ (from-Ξ£-＝ t)
   b : pr₁ (transport B a (f' , g')) ＝ f
   b = pr₁ (transport B a (f' , g')) ＝⟨ t₁ ⟩
       f' ∘ eqtofun e                ＝⟨ refl ⟩
       f                             ∎
   c : transport green-map b (prβ‚‚ (transport B a (f' , g')))  ＝ g
   c = transport green-map b (prβ‚‚ (transport B a (f' , g')))  ＝⟨ refl ⟩
       transport green-map t₁ (prβ‚‚ (transport B a (f' , g'))) ＝⟨ tβ‚‚ ⟩
       green-maps-are-closed-under-precomp-with-equivs e g' ＝⟨ dfunext fe u ⟩
       g ∎
    where
     u : (y : Y) β†’ green-maps-are-closed-under-precomp-with-equivs e g' y ＝ g y
     u y = green-maps-are-closed-under-precomp-with-equivs e g' y ＝⟨ refl ⟩
           transport green (p ⁻¹) (g' y)                          ＝⟨ refl ⟩
           transport green (p ⁻¹) (transport green (q ⁻¹) (g y))  ＝⟨ i ⟩
           transport green (q ⁻¹ βˆ™ p ⁻¹) (g y)                    ＝⟨ ii ⟩
           g y                                                    ∎
       where
        p : fiber (f' ∘ eqtofun e) y ＝ fiber f' y
        p = eqtoid ua _ _ (precomposition-with-equiv-does-not-change-fibers e f' y)
        q : fiber f' y ＝ fiber f y
        q = eqtoid ua (fiber f' y) (fiber f y) (pr₁-fiber-equiv y)
        i  = (transport-βˆ™ green (q ⁻¹) (p ⁻¹)) ⁻¹
        ii = ap (Ξ» - β†’ transport green - (g y)) v
         where
          v = q ⁻¹ βˆ™ p ⁻¹ ＝⟨ ⁻¹-contravariant p q ⟩
              (p βˆ™ q) ⁻¹  ＝⟨ ap (_⁻¹) w ⟩
              refl        ∎
           where
            w : p βˆ™ q ＝ refl
            w = eqtoid ua _ _ Ο• βˆ™ eqtoid ua _ _ ψ ＝⟨ eqtoid-comp ua _ _ ⟩
                eqtoid ua _ _ (Ο• ● ψ)             ＝⟨ ap (eqtoid ua _ _) Ο•Οˆ ⟩
                eqtoid ua _ _ (≃-refl _)          ＝⟨ eqtoid-refl ua _ ⟩
                refl                              ∎
             where
              Ο• : fiber (f' ∘ eqtofun e) y ≃ fiber f' y
              Ο• = precomposition-with-equiv-does-not-change-fibers e f' y
              ψ : fiber pr₁ y ≃ pr₁ (Ο‡ (X , f , g) y)
              ψ = pr₁-fiber-equiv y
              Ο•Οˆ : Ο• ● ψ ＝ ≃-refl (fiber (f' ∘ eqtofun e) y)
              Ο•Οˆ = to-Ξ£-＝ (dfunext fe'' Ο•Οˆ' ,
                           being-equiv-is-prop'' fe'' id _ (id-is-equiv _))
               where
                Ο•Οˆ' : (z : fiber (f' ∘ eqtofun e) y)
                   β†’ eqtofun (Ο• ● ψ) z ＝ z
                Ο•Οˆ' (x , refl) = refl
                fe'' : funext 𝓀 𝓀
                fe'' = univalence-gives-funext ua

 Ο‡-is-equivalence : is-equiv Ο‡
 χ-is-equivalence = (T , χT) , (T , Tχ)

 classification-equivalence : Green-map ≃ (Y β†’ Green)
 classification-equivalence = Ο‡ , Ο‡-is-equivalence

\end{code}

We now can get type-classifier above as a special case of this more
general situation:

\begin{code}

module type-classifier-bis
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 open general-classifier (univalence-gives-funext ua) fe' ua Y (Ξ» (X : 𝓀 Μ‡ ) β†’ πŸ™)

 type-classification-equivalence : (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) ≃ (Y β†’ 𝓀 Μ‡ )
 type-classification-equivalence = (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) β‰ƒβŸ¨ Ο• ⟩
                                   Green-map β‰ƒβŸ¨ classification-equivalence ⟩
                                   (Y β†’ Green) β‰ƒβŸ¨ ψ ⟩
                                   (Y β†’ 𝓀 Μ‡ ) β– 
  where
   Ο• : (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) ≃ Green-map
   Ο• = qinveq Ξ± (Ξ² , a , b)
    where
     Ξ± : (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)) β†’ Green-map
     Ξ± (X , f) = X , (f , (Ξ» y β†’ ⋆))
     Ξ² : Green-map β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y))
     Ξ² (X , f , g) = X , f
     a : (p : Ξ£ (Ξ» X β†’ X β†’ Y)) β†’ Ξ² (Ξ± p) ＝ p
     a (X , f) = refl
     b : (q : Green-map) β†’ Ξ± (Ξ² q) ＝ q
     b (X , f , g) = to-Σ-＝ (refl ,
                             to-Σ-＝ (refl ,
                                     dfunext (univalence-gives-funext ua)
                                      (Ξ» y β†’ πŸ™-is-prop ⋆ (g y))))
   ψ : (Y β†’ Green) ≃ (Y β†’ 𝓀 Μ‡ )
   ψ = β†’cong fe' fe' (≃-refl Y) Ξ³
    where
     Ξ³ : Green ≃ 𝓀 Μ‡
     Ξ³ = qinveq pr₁ ((Ξ» X β†’ (X , ⋆ )) , c , Ξ» x β†’ refl)
      where
       c : (p : Ξ£ (Ξ» X β†’ πŸ™)) β†’ pr₁ p , ⋆ ＝ p
       c (x , ⋆) = refl

\end{code}

And we also get the other examples in the TODO:

\begin{code}

module subsingleton-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 open general-classifier (univalence-gives-funext ua) fe' ua Y
                         (Ξ» (X : 𝓀 Μ‡ ) β†’ is-prop X)

 subsingleton-classification-equivalence : (Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y) ≃ (Y β†’ Ξ© 𝓀 )
 subsingleton-classification-equivalence = classification-equivalence

module singleton-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 open import UF.Subsingletons-FunExt
 open general-classifier (univalence-gives-funext ua) fe' ua Y
                         (Ξ» (X : 𝓀 Μ‡ ) β†’ is-singleton X)

 singleton-classification-equivalence : (Ξ£ X κž‰ 𝓀 Μ‡ , X ≃ Y) ≃ πŸ™ {𝓀}
 singleton-classification-equivalence =
  (Ξ£ X κž‰ 𝓀 Μ‡ , X ≃ Y)                            β‰ƒβŸ¨ i ⟩
  (Ξ£ X κž‰ 𝓀 Μ‡ , (Ξ£ f κž‰ (X β†’ Y), is-vv-equiv f)) β‰ƒβŸ¨ ii ⟩
  (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , is-singleton X))             β‰ƒβŸ¨ iii ⟩
  (Y β†’ πŸ™)                                             β‰ƒβŸ¨ β†’πŸ™ fe ⟩
  πŸ™                                                   β– 
   where
    fe : funext 𝓀 𝓀
    fe = univalence-gives-funext ua

    i   = Ξ£-cong (Ξ» (X : 𝓀 Μ‡ ) β†’ Ξ£-cong (Ξ» (f : X β†’ Y) β†’
           logically-equivalent-props-are-equivalent
            (being-equiv-is-prop'' fe f)
            (Ξ -is-prop fe (Ξ» y β†’ being-singleton-is-prop fe))
            (equivs-are-vv-equivs f)
            (vv-equivs-are-equivs f)))
    ii  = classification-equivalence
    iii = β†’cong fe fe' (≃-refl Y) ψ
     where
      ψ : Ξ£ (Ξ» X β†’ is-singleton X) ≃ πŸ™
      ψ = qinveq unique-to-πŸ™ ((Ξ» _ β†’ πŸ™ , πŸ™-is-singleton) , (a , πŸ™-is-prop ⋆))
       where
       a : (p : Ξ£ (Ξ» v β†’ is-singleton v)) β†’ πŸ™ , πŸ™-is-singleton ＝ p
       a (X , s) = to-Ξ£-＝ (eqtoid ua πŸ™ X (singleton-≃-πŸ™' s) ,
                           being-singleton-is-prop fe _ s)

open import UF.PropTrunc

module inhabited-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
        (pt : propositional-truncations-exist)
       where

 open import UF.ImageAndSurjection pt
 open PropositionalTruncation pt
 open general-classifier (univalence-gives-funext ua) fe' ua Y
                         (Ξ» (X : 𝓀 Μ‡ ) β†’ βˆ₯ X βˆ₯)

 inhabited-classification-equivalence :
  (Ξ£ X κž‰ 𝓀 Μ‡ , (Ξ£ f κž‰ (X β†’ Y), is-surjection f )) ≃
   (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , βˆ₯ X βˆ₯))
 inhabited-classification-equivalence = classification-equivalence

module pointed-classifier
        {𝓀 : Universe}
        (fe' : funext 𝓀 (𝓀 ⁺))
        (ua : is-univalent 𝓀)
        (Y : 𝓀 Μ‡ )
       where

 open import UF.Retracts
 open general-classifier (univalence-gives-funext ua) fe' ua Y (Ξ» (X : 𝓀 Μ‡ ) β†’ X)

 pointed-classification-equivalence :
  (Ξ£ X κž‰ 𝓀 Μ‡ , Y ◁ X) ≃ (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , X))
 pointed-classification-equivalence =
  (Ξ£ X κž‰ 𝓀 Μ‡ , Y ◁ X)                                  β‰ƒβŸ¨ i ⟩
  (Ξ£ X κž‰ 𝓀 Μ‡ , (Ξ£ f κž‰ (X β†’ Y) , ((y : Y) β†’ fiber f y))) β‰ƒβŸ¨ ii ⟩
  (Y β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , X))                                β– 
   where
    i  = Ξ£-cong (Ξ» (X : 𝓀 Μ‡ ) β†’ Ξ£-cong (Ξ» (f : X β†’ Y) β†’ retract-pointed-fibers))
    ii = classification-equivalence

\end{code}