Martin Escardo.

Formulation of univalence. Notice that this file doesn't postulate
univalence. It only defines the notion of univalent
universe. Univalence, when used, is taken as an explicit hypothesis.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

module UF.Univalence where

open import MLTT.Spartan
open import UF.Base
open import UF.Subsingletons
open import UF.Equiv
open import UF.LeftCancellable

is-univalent : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
is-univalent 𝓀 = (X Y : 𝓀 Μ‡ ) β†’ is-equiv (idtoeq X Y)

Univalence : 𝓀ω
Univalence = (𝓀 : Universe) β†’ is-univalent 𝓀

idtoeq' : (X Y : 𝓀 Μ‡ ) β†’ X ＝ Y β†’ X ≃ Y
idtoeq' X Y p = (Idtofun p , transports-are-equivs p)

idtoEqs-agree : (X Y : 𝓀 Μ‡ ) β†’ idtoeq' X Y ∼ idtoeq X Y
idtoEqs-agree X _ refl = refl

Idtofun-is-equiv : (X Y : 𝓀 Μ‡ ) (p : X ＝ Y) β†’ is-equiv(idtofun X Y p)
Idtofun-is-equiv X Y p = prβ‚‚(idtoeq X Y p)

module _
        (ua : is-univalent 𝓀)
       where

 eqtoid : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ X ＝ Y
 eqtoid X Y = pr₁(pr₁(ua X Y))

 idtoeq-eqtoid : (X Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ idtoeq X Y (eqtoid X Y e) ＝ e
 idtoeq-eqtoid X Y = prβ‚‚(pr₁(ua X Y))

 eqtoid-idtoeq : (X Y : 𝓀 Μ‡ ) (p : X ＝ Y) β†’  eqtoid X Y (idtoeq X Y p) ＝ p
 eqtoid-idtoeq X Y = pr₁(prβ‚‚ (equivs-are-qinvs (idtoeq X Y) (ua X Y)))

 eqtoid-refl : (X : 𝓀 Μ‡ ) β†’ eqtoid X X (≃-refl X) ＝ refl
 eqtoid-refl X = eqtoid-idtoeq X X refl

 idtoeq'-eqtoid : (X Y : 𝓀 Μ‡ ) β†’ idtoeq' X Y ∘ eqtoid X Y ∼ id
 idtoeq'-eqtoid X Y e = idtoEqs-agree X Y (eqtoid X Y e) βˆ™ idtoeq-eqtoid X Y e

 idtofun-eqtoid : {X Y : 𝓀 Μ‡ } (e : X ≃ Y)
                β†’ idtofun X Y (eqtoid X Y e) ＝ ⌜ e ⌝
 idtofun-eqtoid {X} {Y} e = ap pr₁ (idtoeq-eqtoid X Y e)

 Idtofun-eqtoid : {X Y : 𝓀 Μ‡ } (e : X ≃ Y)
                β†’ Idtofun (eqtoid X Y e) ＝ ⌜ e ⌝
 Idtofun-eqtoid {X} {Y} e =
  (idtofun-agreement X Y (eqtoid X Y e)) ⁻¹ βˆ™ idtofun-eqtoid e

 Idtofun-βˆ™ : {X Y Z : 𝓀 Μ‡ } (p : X ＝ Y) (q : Y ＝ Z)
           β†’ Idtofun (p βˆ™ q) ＝ Idtofun q ∘ Idtofun p
 Idtofun-βˆ™ refl refl = refl

 univalence-≃ : (X Y : 𝓀 Μ‡ ) β†’ (X ＝ Y) ≃ (X ≃ Y)
 univalence-≃ X Y = idtoeq X Y , ua X Y

 back-transport-is-pre-comp' : {X X' Y : 𝓀 Μ‡ } (e : X ≃ X') (g : X' β†’ Y)
                             β†’ transport⁻¹ (Ξ» - β†’ - β†’ Y) (eqtoid X X' e) g ＝ g ∘ ⌜ e ⌝
 back-transport-is-pre-comp' {X} {X'} e g = transport⁻¹-is-pre-comp (eqtoid X X' e) g βˆ™ q
  where
   q : g ∘ Idtofun (eqtoid X X' e) ＝ g ∘ ⌜ e ⌝
   q = ap (g ∘_) (ap ⌜_⌝ (idtoeq'-eqtoid X X' e))

 pre-comp-is-equiv : {X Y Z : 𝓀 Μ‡ } (f : X β†’ Y)
                   β†’ is-equiv f β†’ is-equiv (Ξ» (g : Y β†’ Z) β†’ g ∘ f)
 pre-comp-is-equiv {X} {Y} f ise =
  equiv-closed-under-∼' (back-transports-are-equivs (eqtoid X Y (f , ise)))
                        (back-transport-is-pre-comp' (f , ise))

\end{code}

Induction on equivalences is available in univalent universes: to
prove that all equivalences satisfy some property, it is enough to
show that the identity equivalences satisfy it.

\begin{code}

≃-induction : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
≃-induction 𝓀 π“₯ = (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
                 β†’ A X (≃-refl X) β†’ (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A Y e

private
 JEq' : is-univalent 𝓀 β†’ βˆ€ {π“₯} β†’ ≃-induction 𝓀 π“₯
 JEq' {𝓀} ua {π“₯} X A b Y e = transport (A Y) (idtoeq-eqtoid ua X Y e) g
  where
   A' : (Y : 𝓀 Μ‡ ) β†’ X ＝ Y β†’ π“₯ Μ‡
   A' Y p = A Y (idtoeq X Y p)
   b' : A' X refl
   b' = b
   f' : (Y : 𝓀 Μ‡ ) (p : X ＝ Y) β†’ A' Y p
   f' = Jbased X A' b'
   g : A Y (idtoeq X Y (eqtoid ua X Y e))
   g = f' Y (eqtoid ua X Y e)

eqtoid-inverse : (ua : is-univalent 𝓀) {X X' : 𝓀 Μ‡ } (e : X ≃ X')
               β†’ (eqtoid ua X X' e)⁻¹ ＝ eqtoid ua X' X (≃-sym e)
eqtoid-inverse ua {X} {X'} = JEq' ua X (Ξ» X' e β†’ (eqtoid ua X X' e)⁻¹ ＝ eqtoid ua X' X (≃-sym e)) p X'
 where
  p : (eqtoid ua X X (≃-refl X))⁻¹ ＝ eqtoid ua X X (≃-sym (≃-refl X))
  p = ap _⁻¹ (eqtoid-refl ua X) βˆ™ (eqtoid-refl ua X)⁻¹

idtofun-eqtoid-⁻¹ : (ua : is-univalent 𝓀) {X Y : 𝓀 Μ‡ } (e : X ≃ Y)
                  β†’ idtofun Y X ((eqtoid ua X Y e) ⁻¹) ＝ ⌜ e ⌝⁻¹
idtofun-eqtoid-⁻¹ ua {X} {Y} e =
 idtofun Y X ((eqtoid ua X Y e) ⁻¹)    ＝⟨ I  ⟩
 idtofun Y X (eqtoid ua Y X (≃-sym e)) ＝⟨ II ⟩
 ⌜ e ⌝⁻¹                               ∎
  where
   I  = ap (idtofun Y X) (eqtoid-inverse ua e)
   II = idtofun-eqtoid ua (≃-sym e)

Idtofun-eqtoid-⁻¹ : (ua : is-univalent 𝓀) {X Y : 𝓀 Μ‡ } (e : X ≃ Y)
                  β†’ Idtofun ((eqtoid ua X Y e) ⁻¹) ＝ ⌜ e ⌝⁻¹
Idtofun-eqtoid-⁻¹ ua {X} {Y} e =
 (idtofun-agreement Y X ((eqtoid ua X Y e) ⁻¹)) ⁻¹ βˆ™ idtofun-eqtoid-⁻¹ ua e

transport-is-pre-comp' : (ua : is-univalent 𝓀)
                       β†’ {X X' : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                         (e : X ≃ X') (g : X β†’ Y)
                       β†’ transport (Ξ» - β†’ - β†’ Y) (eqtoid ua X X' e) g ＝ g ∘ ⌜ e ⌝⁻¹
transport-is-pre-comp' ua {X} {X'} e g = transport-is-pre-comp (eqtoid ua X X' e) g βˆ™ q
 where
  b : Idtofun ((eqtoid ua X X' e)⁻¹) ＝ Idtofun (eqtoid ua X' X (≃-sym e))
  b = ap Idtofun (eqtoid-inverse ua e)
  c : Idtofun (eqtoid ua X' X (≃-sym e)) ＝ pr₁ (≃-sym e)
  c = ap pr₁ (idtoeq'-eqtoid ua X' X (≃-sym e))
  q : g ∘ Idtofun ((eqtoid ua X X' e)⁻¹) ＝ g ∘ pr₁ (≃-sym e)
  q = ap (g ∘_) (b βˆ™ c)

\end{code}

A public, improved version JEq of JEq' is provided below.

Conversely, if the induction principle for equivalences holds, then
univalence follows. In this construction, the parametric universe V is
instantiated to the universe U and its successor 𝓀 ⁺ only. This was
produced 18th May 2018 while visiting the Hausdorff Research Institute
for Mathematics in Bonn.

The following is an adaptation of an 'improvement method' I learned
from Peter Lumsdaine, 7 July 2017, when we were both visiting the
Newton Institute. His original version translated to Agda is here:
http://www.cs.bham.ac.uk/~mhe/TypeTopology/Lumsdaine.html

Unfortunately, we couldn't use his result off-the-shelf. The main
difference is that Peter works with a global identity system on all
types (of a universe), whereas we work with an identity system on a
single type, namely a universe. As a result, we can't define the
type of left-cancellable maps using the notion of equality given by
the identity system, as Peter does. Instead, we define it using the
native (Martin-Loef) identity type, and with this little
modification, Peter's argument goes through for the situation
considered here.

\begin{code}

JEq-improve : βˆ€ {𝓀 π“₯}
            β†’ (jeq' : ≃-induction 𝓀 π“₯)
            β†’ Ξ£ jeq κž‰ ≃-induction 𝓀 π“₯ , ((X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) (b : A X (≃-refl X))
                                      β†’ jeq X A b X (≃-refl X) ＝ b)
JEq-improve {𝓀} {π“₯} jeq' = jeq , jeq-comp
 where
  module _ (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) where
   g : {Y Z : 𝓀 Μ‡ } (p : X ≃ Y) (q : X ≃ Z) β†’ Ξ£ f κž‰ (A Y p β†’ A Z q) , left-cancellable f
   g {Y} {Z} p q = jeq' X B b Z q
    where
     B : (T : 𝓀 Μ‡ ) β†’ X ≃ T β†’ π“₯ Μ‡
     B T q = Ξ£ f κž‰ (A Y p β†’ A T q) , left-cancellable f
     C : (T : 𝓀 Μ‡ ) β†’ X ≃ T β†’ π“₯ Μ‡
     C T p = Ξ£ f κž‰ (A T p β†’ A X (≃-refl X)), left-cancellable f
     b : B X (≃-refl X)
     b = jeq' X C ((Ξ» a β†’ a) , Ξ» p β†’ p) _ p

   h : (b : A X (≃-refl X)) {Y : 𝓀 Μ‡ } (p : X ≃ Y)
     β†’ Ξ£ a κž‰ A Y p , pr₁ (g p p) a ＝ pr₁ (g (≃-refl X) p) b
   h b p = jeq' X B (b , refl) _ p
    where
     B : (Y : 𝓀 Μ‡ ) (p : X ≃ Y) β†’ π“₯ Μ‡
     B Y p = Ξ£ a κž‰ A Y p , pr₁ (g p p) a ＝ pr₁ (g (≃-refl X) p) b

   jeq : A X (≃-refl X) β†’ (Y : 𝓀 Μ‡ ) (p : X ≃ Y) β†’ A Y p
   jeq b Y p = pr₁ (h b p)

   jeq-comp : (b : A X (≃-refl X)) β†’ jeq b X (≃-refl X) ＝ b
   jeq-comp b = prβ‚‚ (g (≃-refl X) (≃-refl X)) (prβ‚‚ (h b (≃-refl X)))

\end{code}

This is the end of Peter's construction, which we apply to our problem
as follows:

\begin{code}

JEq-converse :(βˆ€ {π“₯} β†’ ≃-induction 𝓀 π“₯) β†’ is-univalent 𝓀
JEq-converse {𝓀} jeq' X = Ξ³
 where
  jeq : βˆ€ {π“₯} β†’ ≃-induction 𝓀 π“₯
  jeq {π“₯} = pr₁ (JEq-improve (jeq' {π“₯}))
  jeq-comp : βˆ€ {π“₯} (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) (b : A X (≃-refl X))
          β†’ jeq X A b X (≃-refl X) ＝ b
  jeq-comp {π“₯} = prβ‚‚ (JEq-improve (jeq' {π“₯}))
  Ο† : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ X ＝ Y
  Ο† = jeq X (Ξ» Y p β†’ X ＝ Y) refl
  Ο†c : Ο† X (≃-refl X) ＝ refl
  Ο†c = jeq-comp X (Ξ» Y p β†’ X ＝ Y) refl
  idtoeqΟ† : (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ idtoeq X Y (Ο† Y e) ＝ e
  idtoeqΟ† = jeq X (Ξ» Y e β†’ idtoeq X Y (Ο† Y e) ＝ e) (ap (idtoeq X X) Ο†c)
  Ο†idtoeq : (Y : 𝓀 Μ‡ ) (p : X ＝ Y) β†’ Ο† Y (idtoeq X Y p) ＝ p
  Ο†idtoeq X refl = Ο†c
  Ξ³ : (Y : 𝓀 Μ‡ ) β†’ is-equiv(idtoeq X Y)
  γ Y =  (φ Y , idtoeqφ Y) , (φ Y , φidtoeq Y)

\end{code}

This completes the deduction of univalence from equivalence. Now we
improve our original JEq', to get the computation rule for free (even
if the computation rule holds for the original JEq').

\begin{code}

JEq : is-univalent 𝓀 β†’ βˆ€ {π“₯} β†’ ≃-induction 𝓀 π“₯
JEq ua = pr₁ (JEq-improve (JEq' ua))

JEq-comp : (ua : is-univalent 𝓀) (X : 𝓀 Μ‡ ) (A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ ) (b : A X (≃-refl X))
         β†’ JEq ua X A b X (≃-refl X) ＝ b
JEq-comp ua = prβ‚‚ (JEq-improve (JEq' ua))

\end{code}

A much more transparent and shorter construction of JEq and JEq-comp
is in my MGS'2019 lecture notes and in the module
MGS-Equivalence-induction.

\begin{code}

≃-transport : is-univalent 𝓀
            β†’ βˆ€ {π“₯} (A : 𝓀 Μ‡ β†’ π“₯ Μ‡ ) {X Y : 𝓀 Μ‡ } β†’ X ≃ Y β†’ A X β†’ A Y
≃-transport {𝓀} ua {π“₯} A {X} {Y} e a = JEq ua X (Ξ» Z e β†’ A Z) a Y e

≃-induction' : (𝓀 π“₯ : Universe) β†’ (𝓀 βŠ” π“₯)⁺ Μ‡
≃-induction' 𝓀  π“₯ = (A : (X Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡ )
                 β†’ ((X : 𝓀 Μ‡ ) β†’ A X X (≃-refl X)) β†’ (X Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A X Y e

JEqUnbased : is-univalent 𝓀 β†’ βˆ€ {π“₯} β†’ ≃-induction' 𝓀 π“₯
JEqUnbased ua A f X = JEq ua X (Ξ» Y β†’ A X Y) (f X)

\end{code}

The following technical lemma is needed elsewhere.

\begin{code}

is-univalent-idtoeq-lc : is-univalent 𝓀 β†’ (X Y : 𝓀 Μ‡ ) β†’ left-cancellable(idtoeq X Y)
is-univalent-idtoeq-lc ua X Y = section-lc (idtoeq X Y) (prβ‚‚ (ua X Y))

\end{code}

The following has a proof from function extensionality, but it has a
more direct proof from equivalence induction (we also give a proof
without univalence elsewhere, of course):

\begin{code}

equivs-are-vv-equivs' : is-univalent 𝓀 β†’ {X Y : 𝓀 Μ‡ } (f : X β†’ Y)
                      β†’ is-equiv f β†’ is-vv-equiv f
equivs-are-vv-equivs' {𝓀} ua {X} {Y} f ise = g Y (f , ise)
 where
  A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ 𝓀 Μ‡
  A Y (f , ise) = is-vv-equiv f
  b : A X (≃-refl X)
  b = singleton-types'-are-singletons
  g : (Y : 𝓀 Μ‡ ) (e : X ≃ Y) β†’ A Y e
  g = JEq ua X A b


univalence-gives-propext : is-univalent 𝓀 β†’ propext 𝓀
univalence-gives-propext ua {P} {Q} i j f g = eqtoid ua P Q
                                       (f ,
                                       (g , (Ξ» y β†’ j (f (g y)) y)) ,
                                       (g , (Ξ» x β†’ i (g (f x)) x)))

Univalence-gives-PropExt : Univalence β†’ PropExt
Univalence-gives-PropExt ua 𝓀 = univalence-gives-propext (ua 𝓀)

Univalence-gives-Prop-Ext : Univalence β†’ Prop-Ext
Univalence-gives-Prop-Ext ua {𝓀} = univalence-gives-propext (ua 𝓀)

\end{code}

If the identity function satisfies some property, then all
equivalences do, assuming univalence. This property need not be
prop valued.

\begin{code}

equiv-induction : is-univalent 𝓀
               β†’ (X : 𝓀 Μ‡ )
               β†’ (P : (Y : 𝓀 Μ‡ ) β†’ (X β†’ Y) β†’ π“₯ Μ‡ )
               β†’ P X id
               β†’ (Y : 𝓀 Μ‡ ) (f : X β†’ Y) β†’ is-equiv f β†’ P Y f
equiv-induction {𝓀} {π“₯} ua X P b Y f e = JEq ua X A b Y (f , e)
 where
  A : (Y : 𝓀 Μ‡ ) β†’ X ≃ Y β†’ π“₯ Μ‡
  A Y (f , _) = P Y f

\end{code}