Martin Escardo 1st May 2020.

This 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

\begin{code}

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

module MGS.Classifiers where

open import MGS.Map-Classifiers  public
open import MGS.Embeddings       public
open import MGS.Powerset         public
open import MGS.Universe-Lifting public

Subtypes : 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
Subtypes {𝓀} Y = Ξ£ X κž‰ 𝓀 Μ‡ , X β†ͺ Y

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

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

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

mc-gives-sc : is-map-classifier 𝓀
            β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) β†’ is-special-map-classifier P

mc-gives-sc {𝓀} s P Y = Ξ³
 where
  e = (𝓀 /[ P ] Y)                               β‰ƒβŸ¨ ≃-sym a ⟩
      (Ξ£ Οƒ κž‰ 𝓀 / Y , ((y : Y) β†’ P ((Ο‡ Y) Οƒ y)))  β‰ƒβŸ¨ ≃-sym b ⟩
      (Ξ£ A κž‰ (Y β†’ 𝓀 Μ‡ ), ((y : Y) β†’ P (A y)))     β‰ƒβŸ¨ ≃-sym c ⟩
      (Y β†’ Ξ£ P)                                  β– 
   where
    a = Ξ£-assoc
    b = Ξ£-change-of-variable (Ξ» A β†’ Ξ  (P ∘ A)) (Ο‡ Y) (s Y)
    c = Ξ Ξ£-distr-≃

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

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

Ο‡-special-is-equiv : is-univalent 𝓀 β†’ dfunext 𝓀 (𝓀 ⁺)
                   β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Y : 𝓀 Μ‡ )
                   β†’ is-equiv (Ο‡-special P Y)

Ο‡-special-is-equiv {𝓀} ua fe P Y = mc-gives-sc (universes-are-map-classifiers ua fe) P Y

special-map-classifier : is-univalent 𝓀 β†’ dfunext 𝓀 (𝓀 ⁺)
                       β†’ (P : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) (Y : 𝓀 Μ‡ )
                       β†’ 𝓀 /[ P ] Y ≃ (Y β†’ Ξ£ P)

special-map-classifier {𝓀} ua fe P Y = Ο‡-special P Y , Ο‡-special-is-equiv ua fe P Y

Ξ©-is-subtype-classifier : Univalence
                        β†’ (Y : 𝓀 Μ‡ ) β†’ Subtypes Y ≃ (Y β†’ Ξ© 𝓀)

Ξ©-is-subtype-classifier {𝓀} ua = special-map-classifier (ua 𝓀)
                                  (univalence-gives-dfunext' (ua 𝓀) (ua (𝓀 ⁺)))
                                  is-subsingleton

subtypes-form-set : Univalence β†’ (Y : 𝓀 Μ‡ ) β†’ is-set (Subtypes Y)
subtypes-form-set {𝓀} ua Y = equiv-to-set
                              (Ξ©-is-subtype-classifier ua Y)
                              (powersets-are-sets' ua)

𝓒 : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
𝓒 𝓀 = Ξ£ S κž‰ 𝓀 Μ‡ , is-singleton S

equiv-classification : Univalence
                     β†’ (Y : 𝓀 Μ‡ ) β†’ (Ξ£ X κž‰ 𝓀 Μ‡ , X ≃ Y) ≃ (Y β†’ 𝓒 𝓀)

equiv-classification {𝓀} ua = special-map-classifier (ua 𝓀)
                               (univalence-gives-dfunext' (ua 𝓀) (ua (𝓀 ⁺)))
                               is-singleton

the-singletons-form-a-singleton : propext 𝓀 β†’ dfunext 𝓀 𝓀 β†’ is-singleton (𝓒 𝓀)
the-singletons-form-a-singleton {𝓀} pe fe = c , Ο†
 where
  i : is-singleton (Lift 𝓀 πŸ™)
  i = equiv-to-singleton (Lift-≃ πŸ™) πŸ™-is-singleton

  c : 𝓒 𝓀
  c = Lift 𝓀 πŸ™ , i

  Ο† : (x : 𝓒 𝓀) β†’ c ＝ x
  Ο† (S , s) = to-subtype-＝ (Ξ» _ β†’ being-singleton-is-subsingleton fe) p
   where
    p : Lift 𝓀 πŸ™ ＝ S
    p = pe (singletons-are-subsingletons (Lift 𝓀 πŸ™) i)
           (singletons-are-subsingletons S s)
           (Ξ» _ β†’ center S s) (Ξ» _ β†’ center (Lift 𝓀 πŸ™) i)

univalence→-again : Univalence
                  β†’ (Y : 𝓀 Μ‡ ) β†’ is-singleton (Ξ£ X κž‰ 𝓀 Μ‡ , X ≃ Y)

univalenceβ†’-again {𝓀} ua Y = equiv-to-singleton (equiv-classification ua Y) i
 where
  i : is-singleton (Y β†’ 𝓒 𝓀)
  i = univalence-gives-vvfunext' (ua 𝓀) (ua (𝓀 ⁺))
        (Ξ» y β†’ the-singletons-form-a-singleton
                (univalence-gives-propext (ua 𝓀))
                (univalence-gives-dfunext (ua 𝓀)))

\end{code}