Martin Escardo 8th May 2020.

An obsolete, clumsy version of this file is at UF.Classifiers-Old.

This version is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

but with the universe levels generalized and Ξ£-fibers added in
September 2022.

   * Universes are map classifiers.
   * Ξ© 𝓀 is the embedding classifier.
   * The type of pointed types is the retraction classifier.
   * The type inhabited types is the surjection classifier.
   * The fibers of Ξ£ are non-dependent function types.

\begin{code}

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

module UF.Classifiers where

open import MLTT.Spartan
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Powerset hiding (𝕋)
open import UF.Retracts
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.SubtypeClassifier
open import UF.UA-FunExt
open import UF.Univalence

\end{code}

The slice type:

\begin{code}

_/_ : (𝓀 : Universe) β†’ π“₯ Μ‡ β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
𝓀 / Y = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ Y)

\end{code}

A modification of the slice type, where P doesn't need to be
proposition-valued and so can add structure. An example is P = id,
which is studied below in connection with retractions.

\begin{code}

_/[_]_ : (𝓀 : Universe) β†’ (𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ ) β†’ π“₯ Μ‡ β†’ 𝓀 ⁺ βŠ” π“₯ βŠ” 𝓦 Μ‡
𝓀 /[ P ] Y = Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , ((y : Y) β†’ P (fiber f y))

\end{code}

We first consider the original situation of the MGS development with a
single universe for comparison.

\begin{code}

module classifier-single-universe (𝓀 : Universe) where

 Ο‡ : (Y : 𝓀 Μ‡ ) β†’ 𝓀 / Y  β†’ (Y β†’ 𝓀 Μ‡ )
 Ο‡ Y (X , f) = fiber f

 universe-is-classifier : 𝓀 ⁺ Μ‡
 universe-is-classifier = (Y : 𝓀 Μ‡ ) β†’ is-equiv (Ο‡ Y)

 𝕋 : (Y : 𝓀 Μ‡ ) β†’ (Y β†’ 𝓀 Μ‡ ) β†’ 𝓀 / Y
 𝕋 Y A = Ξ£ A , pr₁

 χη : is-univalent 𝓀
    β†’ (Y : 𝓀 Μ‡ ) (Οƒ : 𝓀 / Y) β†’ 𝕋 Y (Ο‡ Y Οƒ) ＝ Οƒ
 χη ua Y (X , f) = r
  where
   e : Ξ£ (fiber f) ≃ X
   e = total-fiber-is-domain f

   p : Σ (fiber f) ＝ X
   p = eqtoid ua (Ξ£ (fiber f)) X e

   NB : ⌜ e ⌝⁻¹ ＝ (Ξ» x β†’ f x , x , refl)
   NB = refl

   q = transport (Ξ» - β†’ - β†’ Y) p pr₁ ＝⟨ transport-is-pre-comp' ua e pr₁ ⟩
       pr₁ ∘ ⌜ e ⌝⁻¹                 ＝⟨ refl ⟩
       f                             ∎

   r : (Ξ£ (fiber f) , pr₁) ＝ (X , f)
   r = to-Σ-＝ (p , q)

 χΡ : is-univalent 𝓀
    β†’ funext 𝓀 (𝓀 ⁺)
    β†’ (Y : 𝓀 Μ‡ ) (A : Y β†’ 𝓀 Μ‡ ) β†’ Ο‡ Y (𝕋 Y A) ＝ A
 χΡ ua fe Y A = dfunext fe Ξ³
  where
   f : βˆ€ y β†’ fiber pr₁ y β†’ A y
   f y ((y , a) , refl) = a

   g : βˆ€ y β†’ A y β†’ fiber pr₁ y
   g y a = (y , a) , refl

   Ξ· : βˆ€ y Οƒ β†’ g y (f y Οƒ) ＝ Οƒ
   Ξ· y ((y , a) , refl) = refl

   Ξ΅ : βˆ€ y a β†’ f y (g y a) ＝ a
   Ξ΅ y a = refl

   Ξ³ : βˆ€ y β†’ fiber pr₁ y ＝ A y
   Ξ³ y = eqtoid ua _ _ (qinveq (f y) (g y , Ξ· y , Ξ΅ y))

 universes-are-classifiers : is-univalent 𝓀
                           β†’ funext 𝓀 (𝓀 ⁺)
                           β†’ universe-is-classifier
 universes-are-classifiers ua fe Y = qinvs-are-equivs (Ο‡ Y)
                                      (𝕋 Y , χη ua Y , χΡ ua fe Y)

 classification : is-univalent 𝓀
                β†’ funext 𝓀 (𝓀 ⁺)
                β†’ (Y : 𝓀 Μ‡ )
                β†’ 𝓀 / Y ≃ (Y β†’ 𝓀 Μ‡ )
 classification ua fe Y = Ο‡ Y , universes-are-classifiers ua fe Y

module special-classifier-single-universe (𝓀 : Universe) where

 open classifier-single-universe 𝓀

 Ο‡-special : (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Y : 𝓀 Μ‡ ) β†’ 𝓀 /[ P ] Y  β†’ (Y β†’ Ξ£ P)
 Ο‡-special P Y (X , f , Ο†) y = fiber f y , Ο† y

 universe-is-special-classifier : (𝓀 Μ‡ β†’ π“₯ Μ‡ ) β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡
 universe-is-special-classifier P = (Y : 𝓀 Μ‡ ) β†’ is-equiv (Ο‡-special P Y)

 classifier-gives-special-classifier : universe-is-classifier
                                     β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ )
                                     β†’ universe-is-special-classifier P
 classifier-gives-special-classifier s P Y = Ξ³
  where
   e = (𝓀 /[ P ] Y)                               β‰ƒβŸ¨ a ⟩
       (Ξ£ Οƒ κž‰ 𝓀 / Y , ((y : Y) β†’ P ((Ο‡ Y) Οƒ y)))  β‰ƒβŸ¨ b ⟩
       (Ξ£ A κž‰ (Y β†’ 𝓀 Μ‡ ), ((y : Y) β†’ P (A y)))     β‰ƒβŸ¨ c ⟩
       (Y β†’ Ξ£ P)                                  β– 
    where
     a = ≃-sym Ξ£-assoc
     b = Ξ£-change-of-variable (Ξ» A β†’ Ξ  (P ∘ A)) (Ο‡ Y) (s Y)
     c = ≃-sym Ξ Ξ£-distr-≃

   NB : Ο‡-special P Y ＝ ⌜ e ⌝
   NB = refl

   Ξ³ : is-equiv (Ο‡-special P Y)
   γ = ⌜⌝-is-equiv e

 Ο‡-special-is-equiv : is-univalent 𝓀
                    β†’ funext 𝓀 (𝓀 ⁺)
                    β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Y : 𝓀 Μ‡ )
                    β†’ is-equiv (Ο‡-special P Y)
 Ο‡-special-is-equiv ua fe P Y = classifier-gives-special-classifier
                                 (universes-are-classifiers ua fe) P Y

 special-classification : is-univalent 𝓀
                        β†’ funext 𝓀 (𝓀 ⁺)
                        β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Y : 𝓀 Μ‡ )
                        β†’ 𝓀 /[ P ] Y ≃ (Y β†’ Ξ£ P)
 special-classification ua fe P Y = Ο‡-special P Y , Ο‡-special-is-equiv ua fe P Y

\end{code}

Some examples of special classifiers follow.

The universe of pointed types classifies retractions:

\begin{code}

module retraction-classifier (𝓀 : Universe) where

 open special-classifier-single-universe 𝓀

 retractions-into : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
 retractions-into Y = Ξ£ X κž‰ 𝓀 Μ‡ , Y ◁ X

 pointed-types : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
 pointed-types 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , X

 retraction-classifier : Univalence
                       β†’ (Y : 𝓀 Μ‡ ) β†’ retractions-into Y ≃ (Y β†’ pointed-types 𝓀)
 retraction-classifier ua Y =
  retractions-into Y     β‰ƒβŸ¨ i ⟩
  ((𝓀 /[ id ] Y))        β‰ƒβŸ¨ ii ⟩
  (Y β†’ pointed-types 𝓀)  β– 
  where
   i  = ≃-sym (Ξ£-cong (Ξ» X β†’ Ξ£-cong (Ξ» f β†’ Ξ Ξ£-distr-≃)))
   ii = special-classification (ua 𝓀)
         (univalence-gives-funext' 𝓀 (𝓀 ⁺) (ua 𝓀) (ua (𝓀 ⁺)))
         id Y

\end{code}

The universe of inhabited types classifies surjections:

\begin{code}

module surjection-classifier (𝓀 : Universe) where

 open special-classifier-single-universe 𝓀

 open import UF.PropTrunc

 module _ (pt : propositional-truncations-exist) where

  open PropositionalTruncation pt public
  open import UF.ImageAndSurjection pt public

  surjections-into : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
  surjections-into Y = Ξ£ X κž‰ 𝓀 Μ‡ , X β†  Y

  inhabited-types : 𝓀 ⁺ Μ‡
  inhabited-types = Ξ£ X κž‰ 𝓀 Μ‡ , βˆ₯ X βˆ₯

  surjection-classification : Univalence
                            β†’ (Y : 𝓀 Μ‡ )
                            β†’ surjections-into Y ≃ (Y β†’ inhabited-types)
  surjection-classification ua =
   special-classification (ua 𝓀)
     (univalence-gives-funext' 𝓀 (𝓀 ⁺) (ua 𝓀) (ua (𝓀 ⁺)))
     βˆ₯_βˆ₯

\end{code}

Added 11th September 2022. We now generalize the universe levels of
the classifier and special classifier modules.

\begin{code}

module classifier (𝓀 π“₯ : Universe) where

 Ο‡ : (Y : 𝓀 Μ‡ ) β†’ (𝓀 βŠ” π“₯) / Y  β†’ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ )
 Ο‡ Y (X , f) = fiber f

\end{code}

Definition of when the given pair of universes is a classifier,

\begin{code}

 universe-is-classifier : (𝓀 βŠ” π“₯)⁺ Μ‡
 universe-is-classifier = (Y : 𝓀 Μ‡ ) β†’ is-equiv (Ο‡ Y)

 𝕋 : (Y : 𝓀 Μ‡ ) β†’ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ (𝓀 βŠ” π“₯) / Y
 𝕋 Y A = Ξ£ A , pr₁

 χη : is-univalent (𝓀 βŠ” π“₯)
    β†’ (Y : 𝓀 Μ‡ ) (Οƒ : (𝓀 βŠ” π“₯) / Y) β†’ 𝕋 Y (Ο‡ Y Οƒ) ＝ Οƒ
 χη ua Y (X , f) = r
  where
   e : Ξ£ (fiber f) ≃ X
   e = total-fiber-is-domain f

   p : Σ (fiber f) ＝ X
   p = eqtoid ua (Ξ£ (fiber f)) X e

   NB : ⌜ e ⌝⁻¹ ＝ (Ξ» x β†’ f x , x , refl)
   NB = refl

   q = transport (Ξ» - β†’ - β†’ Y) p pr₁ ＝⟨ transport-is-pre-comp' ua e pr₁ ⟩
       pr₁ ∘ ⌜ e ⌝⁻¹                 ＝⟨ refl ⟩
       f                             ∎

   r : (Ξ£ (fiber f) , pr₁) ＝ (X , f)
   r = to-Σ-＝ (p , q)

 χΡ : is-univalent (𝓀 βŠ” π“₯)
    β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
    β†’ (Y : 𝓀 Μ‡ ) (A : Y β†’ 𝓀 βŠ” π“₯ Μ‡ ) β†’ Ο‡ Y (𝕋 Y A) ＝ A
 χΡ ua fe Y A = dfunext fe Ξ³
  where
   f : βˆ€ y β†’ fiber pr₁ y β†’ A y
   f y ((y , a) , refl) = a

   g : βˆ€ y β†’ A y β†’ fiber pr₁ y
   g y a = (y , a) , refl

   Ξ· : βˆ€ y Οƒ β†’ g y (f y Οƒ) ＝ Οƒ
   Ξ· y ((y , a) , refl) = refl

   Ξ΅ : βˆ€ y a β†’ f y (g y a) ＝ a
   Ξ΅ y a = refl

   Ξ³ : βˆ€ y β†’ fiber pr₁ y ＝ A y
   Ξ³ y = eqtoid ua _ _ (qinveq (f y) (g y , Ξ· y , Ξ΅ y))

 universes-are-classifiers : is-univalent (𝓀 βŠ” π“₯)
                           β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                           β†’ universe-is-classifier
 universes-are-classifiers ua fe Y = qinvs-are-equivs (Ο‡ Y)
                                          (𝕋 Y , χη ua Y , χΡ ua fe Y)

 classification : is-univalent (𝓀 βŠ” π“₯)
                β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                β†’ (Y : 𝓀 Μ‡ )
                β†’ (𝓀 βŠ” π“₯) / Y ≃ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ )
 classification ua fe Y = Ο‡ Y , universes-are-classifiers ua fe Y

\end{code}

In the case of special classifiers we now need to assume a further
universe 𝓦.

\begin{code}

module special-classifier (𝓀 π“₯ 𝓦 : Universe) where

 open classifier 𝓀 π“₯ public

 Ο‡-special : (P : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ ) (Y : 𝓀 Μ‡ ) β†’ (𝓀 βŠ” π“₯) /[ P ] Y  β†’ (Y β†’ Ξ£ P)
 Ο‡-special P Y (X , f , Ο†) y = fiber f y , Ο† y

 universe-is-special-classifier : (𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ ) β†’ (𝓀 βŠ” π“₯)⁺ βŠ” 𝓦 Μ‡
 universe-is-special-classifier P = (Y : 𝓀 Μ‡ ) β†’ is-equiv (Ο‡-special P Y)

 classifier-gives-special-classifier : universe-is-classifier
                                     β†’ (P : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ )
                                     β†’ universe-is-special-classifier P
 classifier-gives-special-classifier s P Y = Ξ³
  where
   e = ((𝓀 βŠ” π“₯) /[ P ] Y)                               β‰ƒβŸ¨ a ⟩
       (Ξ£ Οƒ κž‰ (𝓀 βŠ” π“₯) / Y , ((y : Y) β†’ P ((Ο‡ Y) Οƒ y)))  β‰ƒβŸ¨ b ⟩
       (Ξ£ A κž‰ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ ), ((y : Y) β†’ P (A y)))       β‰ƒβŸ¨ c ⟩
       (Y β†’ Ξ£ P)                                        β– 
    where
     a = ≃-sym Ξ£-assoc
     b = Ξ£-change-of-variable (Ξ» A β†’ Ξ  (P ∘ A)) (Ο‡ Y) (s Y)
     c = ≃-sym Ξ Ξ£-distr-≃

   NB : Ο‡-special P Y ＝ ⌜ e ⌝
   NB = refl

   Ξ³ : is-equiv (Ο‡-special P Y)
   γ = ⌜⌝-is-equiv e

 Ο‡-special-is-equiv : is-univalent (𝓀 βŠ” π“₯)
                    β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                    β†’ (P : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ ) (Y : 𝓀 Μ‡ )
                    β†’ is-equiv (Ο‡-special P Y)
 Ο‡-special-is-equiv ua fe P Y = classifier-gives-special-classifier
                                 (universes-are-classifiers ua fe) P Y

 special-classification : is-univalent (𝓀 βŠ” π“₯)
                        β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                        β†’ (P : 𝓀 βŠ” π“₯ Μ‡ β†’ 𝓦 Μ‡ ) (Y : 𝓀 Μ‡ )
                        β†’ (𝓀 βŠ” π“₯) /[ P ] Y ≃ (Y β†’ Ξ£ P)
 special-classification ua fe P Y = Ο‡-special P Y , Ο‡-special-is-equiv ua fe P Y

\end{code}

The subtype classifier with general universes:

\begin{code}

Ξ©-is-subtype-classifier' : is-univalent (𝓀 βŠ” π“₯)
                         β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
                         β†’ (Y : 𝓀 Μ‡ )
                         β†’ Subtype' (𝓀 βŠ” π“₯) Y ≃ (Y β†’ Ξ© (𝓀 βŠ” π“₯))
Ξ©-is-subtype-classifier' {𝓀} {π“₯} ua fe = special-classification ua fe
                                          is-subsingleton
 where
  open special-classifier 𝓀 π“₯ (𝓀 βŠ” π“₯)

Ξ©-is-subtype-classifier : is-univalent 𝓀
                        β†’ funext 𝓀 (𝓀 ⁺)
                        β†’ (Y : 𝓀 Μ‡ )
                        β†’ Subtype Y ≃ (Y β†’ Ξ© 𝓀)
Ξ©-is-subtype-classifier {𝓀} = Ξ©-is-subtype-classifier' {𝓀} {𝓀}

subtypes-form-set : Univalence β†’ (Y : 𝓀 Μ‡ ) β†’ is-set (Subtype' (𝓀 βŠ” π“₯) Y)
subtypes-form-set {𝓀} {π“₯} ua Y =
 equiv-to-set
  (Ξ©-is-subtype-classifier' {𝓀} {π“₯}
    (ua (𝓀 βŠ” π“₯))
    (univalence-gives-funext' 𝓀 ((𝓀 βŠ” π“₯)⁺)
      (ua 𝓀)
      (ua ((𝓀 βŠ” π“₯)⁺)))
    Y)
  (powersets-are-sets''
    (univalence-gives-funext' _ _ (ua 𝓀) (ua ((𝓀 βŠ” π“₯)⁺)))
    (univalence-gives-funext' _ _ (ua (𝓀 βŠ” π“₯)) (ua (𝓀 βŠ” π“₯)))
    (univalence-gives-propext (ua (𝓀 βŠ” π“₯))))

\end{code}

9th September 2022, with universe levels generalized 11
September. Here is an application of the above.

\begin{code}

Ξ£-fibers-≃ : {𝓀 π“₯ : Universe}
           β†’ is-univalent (𝓀 βŠ” π“₯)
           β†’ funext 𝓀 ((𝓀 βŠ” π“₯)⁺)
           β†’ {X : 𝓀 βŠ” π“₯ Μ‡ } {Y : 𝓀 Μ‡ }
           β†’ (Ξ£ A κž‰ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ ) , Ξ£ A ≃ X) ≃ (X β†’ Y)
Ξ£-fibers-≃ {𝓀} {π“₯} ua fe⁺ {X} {Y} =
  (Ξ£ A κž‰ (Y β†’ 𝓀 βŠ” π“₯ Μ‡ ) , Ξ£ A ≃ X)                            β‰ƒβŸ¨ I ⟩
  (Ξ£ (Z , g) κž‰ (𝓀 βŠ” π“₯) / Y , (Ξ£ y κž‰ Y , fiber g y) ≃ X)      β‰ƒβŸ¨ II ⟩
  (Ξ£ Z κž‰ 𝓀 βŠ” π“₯ Μ‡ , Ξ£ g κž‰ (Z β†’ Y) , (Ξ£ y κž‰ Y , fiber g y) ≃ X) β‰ƒβŸ¨ III ⟩
  (Ξ£ Z κž‰ 𝓀 βŠ” π“₯ Μ‡ , (Z β†’ Y) Γ— (Z ≃ X))                         β‰ƒβŸ¨ IV ⟩
  (Ξ£ Z κž‰ 𝓀 βŠ” π“₯ Μ‡ , (Z ≃ X) Γ— (Z β†’ Y))                         β‰ƒβŸ¨ V ⟩
  (Ξ£ Z κž‰ 𝓀 βŠ” π“₯ Μ‡ , (X ≃ Z) Γ— (Z β†’ Y))                         β‰ƒβŸ¨ VI ⟩
  (Ξ£ (Z , _) κž‰ (Ξ£ Z κž‰ 𝓀 βŠ” π“₯ Μ‡ , X ≃ Z) , (Z β†’ Y))             β‰ƒβŸ¨ VII ⟩
  (X β†’ Y)                                                    β– 
 where
  open classifier 𝓀 π“₯
  open import UF.Equiv-FunExt
  open import UF.PropIndexedPiSigma
  open import UF.Yoneda

  fe : funext (𝓀 βŠ” π“₯) (𝓀 βŠ” π“₯)
  fe = univalence-gives-funext ua

  I   = ≃-sym (Ξ£-change-of-variable (Ξ» A β†’ Ξ£ A ≃ X) (Ο‡ Y)
               (universes-are-classifiers ua fe⁺ Y))
  II  = Ξ£-assoc
  III = Ξ£-cong (Ξ» Z β†’ Ξ£-cong (Ξ» g β†’ ≃-cong-left' fe fe fe fe fe
                                     (total-fiber-is-domain g)))
  IV  = Ξ£-cong (Ξ» Z β†’ Γ—-comm)
  V   = Ξ£-cong (Ξ» Z β†’ Γ—-cong (≃-Sym' fe fe fe fe) (≃-refl (Z β†’ Y)))
  VI  = ≃-sym Ξ£-assoc
  VII = prop-indexed-sum
         (X , ≃-refl X)
         (singletons-are-props
           (univalence-via-singletons→ ua X))

private
 βˆ‘ : {𝓀 π“₯ : Universe} (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡
 βˆ‘ X Y = Ξ£ Y

\end{code}

The use of equality rather than equivalence prevents us from having
more general universes in the following:

\begin{code}

Ξ£-fibers : is-univalent 𝓀
         β†’ funext 𝓀 (𝓀 ⁺)
         β†’ {X Y : 𝓀 Μ‡ }
         β†’ fiber (βˆ‘ Y) X ≃ (X β†’ Y)
Ξ£-fibers {𝓀} ua fe⁺ {X} {Y} =
  (Ξ£ A κž‰ (Y β†’ 𝓀 Μ‡ ) , Ξ£ A ＝ X) β‰ƒβŸ¨ Ξ£-cong (Ξ» A β†’ univalence-≃ ua (Ξ£ A) X) ⟩
  (Ξ£ A κž‰ (Y β†’ 𝓀 Μ‡ ) , Ξ£ A ≃ X)  β‰ƒβŸ¨ Ξ£-fibers-≃ {𝓀} {𝓀} ua fe⁺ ⟩
  (X β†’ Y)                       β– 

\end{code}

Added 22nd June 2025 by Martin Escardo, from an old draft.

If a universe 𝓀 is a classifier, then it is univalent, assuming
function extensionality from functions from with domains in 𝓀 and
codomain in 𝓀⁺, and also assuming extensionality for propositions in
the universe 𝓀.

\begin{code}

open import UF.Equiv-FunExt
open import UF.Lower-FunExt
open import UF.Subsingletons-FunExt
open import UF.Yoneda
open import UF.Singleton-Properties

open classifier-single-universe

universe-is-classifier-implies-universe-is-univalent
 : funext 𝓀 (𝓀 ⁺)
 β†’ propext 𝓀
 β†’ universe-is-classifier 𝓀
 β†’ is-univalent 𝓀
universe-is-classifier-implies-universe-is-univalent {𝓀} fe⁺ pe c = V
 where
  fe : funext 𝓀 𝓀
  fe = lower-funext 𝓀 (𝓀 ⁺) fe⁺

  open special-classifier 𝓀 𝓀 𝓀

  P : 𝓀 Μ‡ β†’ 𝓀 Μ‡
  P = is-singleton

  module _ (Y : 𝓀 Μ‡ ) where

   I : (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , ((y : Y) β†’ P (fiber f y))) ≃ (Y β†’ Ξ£ P)
   I = Ο‡-special P Y , classifier-gives-special-classifier c P Y

   _ : (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , ((y : Y) β†’ P (fiber f y)))
    ＝ (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , is-vv-equiv f)
   _ = refl

   II : is-singleton (Y β†’ Ξ£ P)
   II = Ξ -is-singleton fe⁺ (Ξ» _ β†’ the-singletons-form-a-singleton-type fe pe)

   III : is-singleton (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , is-vv-equiv f)
   III = equiv-to-singleton I II

   IV : is-singleton (Ξ£ X κž‰ 𝓀 Μ‡ , (Y ≃ X))
   IV = equiv-to-singleton
         ((Ξ£ X κž‰ 𝓀 Μ‡ , (Y ≃ X))                        β‰ƒβŸ¨ IVβ‚€ ⟩
          (Ξ£ X κž‰ 𝓀 Μ‡ , (X ≃ Y))                        β‰ƒβŸ¨ ≃-refl _ ⟩
          (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , is-equiv f)     β‰ƒβŸ¨ IV₁ ⟩
          (Ξ£ X κž‰ 𝓀 Μ‡ , Ξ£ f κž‰ (X β†’ Y) , is-vv-equiv f)  β– )
        III
         where
          IVβ‚€ = Ξ£-cong (Ξ» X β†’ ≃-sym (≃-flip' fe fe fe fe))
          IV₁ = Ξ£-cong (Ξ» X β†’
                Ξ£-cong (Ξ» f β†’
                 logically-equivalent-props-are-equivalent
                  (being-equiv-is-prop'' fe f)
                  (being-vv-equiv-is-prop' fe fe f)
                  (equivs-are-vv-equivs f)
                  (vv-equivs-are-equivs f)))

  V : is-univalent 𝓀
  V = univalence-via-singletons← IV

\end{code}

Question. Is it possible to remove the extensionality assumptions?