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 --safe --without-K #-} 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 = inverse (idtoeq X Y) (ua X Y) idtoeq-eqtoid : (X Y : π€ Μ ) (e : X β Y) β idtoeq X Y (eqtoid X Y e) οΌ e idtoeq-eqtoid X Y = inverses-are-sections (idtoeq X Y) (ua X Y) eqtoid-idtoeq : (X Y : π€ Μ ) (p : X οΌ Y) β eqtoid X Y (idtoeq X Y p) οΌ p eqtoid-idtoeq X Y = inverses-are-retractions (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 β_β (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'} {Y} e g = Ξ³ where q : g β Idtofun (eqtoid X X' e) οΌ g β β e β q = ap (g β_) (ap β_β (idtoeq'-eqtoid X X' e)) Ξ³ : transportβ»ΒΉ (Ξ» - β - β Y) (eqtoid X X' e) g οΌ g β β e β Ξ³ = transportβ»ΒΉ-is-pre-comp (eqtoid X X' e) g β q 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. NB. There is a more conceptual, and shorter derivation of the following few things in my MGS'2019 lecture notes (included here in the folder MGS). \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'} = Ξ³ 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)β»ΒΉ Ξ³ : (e : X β X') β (eqtoid ua X X' e)β»ΒΉ οΌ eqtoid ua X' X (β-sym e) Ξ³ = JEq' ua X (Ξ» X' e β (eqtoid ua X X' e)β»ΒΉ οΌ eqtoid ua X' X (β-sym e)) p 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'} {Y} e g = Ξ³ 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) Ξ³ : transport (Ξ» - β - β Y) (eqtoid ua X X' e) g οΌ g β β e ββ»ΒΉ Ξ³ = transport-is-pre-comp (eqtoid ua X X' e) g β q \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. The following improvement method is not needed in the approach of the MGS'2019 lecture notes (included here in the folder MGS). \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 abstract 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'). We remark again that the improvement method is not needed, referring the reader to the MGS'2019 lecture notes and alternatively the MGS folder included in this development. \begin{code} abstract 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}