From 86012d841b3c8e270a73bced691a37d646129ee9 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 24 Apr 2015 18:51:16 -0400 Subject: [PATCH] fix(hott): make f explicit in is_equiv.mk and a bit of renaming in init --- hott/arity.hlean | 6 +++--- hott/init/axioms/funext_of_ua.hlean | 2 +- hott/init/axioms/funext_varieties.hlean | 7 +++---- hott/init/equiv.hlean | 19 +++++++++++-------- hott/init/function.hlean | 4 +--- hott/init/trunc.hlean | 18 ++++++++---------- hott/types/eq.hlean | 6 +++--- hott/types/equiv.hlean | 2 +- 8 files changed, 31 insertions(+), 33 deletions(-) diff --git a/hott/arity.hlean b/hott/arity.hlean index 72f1709f53..55f226ee62 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -112,8 +112,8 @@ namespace eq : eq_of_homotopy2 (λa b, idpath (f a b)) = idpath f := begin apply concat, - {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy_id}, - apply eq_of_homotopy_id + {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy_idp}, + apply eq_of_homotopy_idp end definition eq_of_homotopy3_id (f : Πa b c, D a b c) @@ -121,7 +121,7 @@ namespace eq begin apply concat, {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id}, - apply eq_of_homotopy_id + apply eq_of_homotopy_idp end end eq diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index 0685535f07..6a20264b4f 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -151,7 +151,7 @@ definition eq_of_homotopy [reducible] : f ∼ g → f = g := (@apd10 A P f g)⁻¹ --TODO: rename to eq_of_homotopy_idp -definition eq_of_homotopy_id (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := +definition eq_of_homotopy_idp (f : Π x, P x) : eq_of_homotopy (λx : A, idpath (f x)) = idpath f := is_equiv.sect apd10 idp definition naive_funext_of_ua : naive_funext := diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index c3b442536a..2d978d2dd5 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -25,7 +25,6 @@ definition funext.{l k} := Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g) -- Naive funext is the simple assertion that pointwise equal functions are equal. --- TODO think about universe levels definition naive_funext := Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g @@ -67,7 +66,7 @@ section have t2 : is_contr (Πx, Σ y, f x = y), from !wf, have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h, - from @center_eq (Π x, Σ y, f x = y) t2 _ _, + from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _, have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h), from ap r t3, have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h, @@ -80,12 +79,12 @@ section definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h := @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h) - (@center_eq _ is_contr_sigma_homotopy _ _) d + (@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d local attribute weak_funext [reducible] local attribute homotopy_ind [reducible] definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d := - (@hprop_eq_of_is_contr _ _ _ _ !center_eq idp)⁻¹ ▹ idp + (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp end -- Now the proof is fairly easy; we can just use the same induction principle on both sides. diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index b21894be81..c604cff198 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -17,6 +17,7 @@ open eq function -- This is our definition of equivalence. In the HoTT-book it's called -- ihae (half-adjoint equivalence). structure is_equiv [class] {A B : Type} (f : A → B) := +mk' :: (inv : B → A) (retr : (f ∘ inv) ∼ id) (sect : (inv ∘ f) ∼ id) @@ -33,19 +34,22 @@ structure equiv (A B : Type) := namespace is_equiv /- Some instances and closure properties of equivalences -/ postfix `⁻¹` := inv - --a second notation for the inverse, which is not overloaded + /- a second notation for the inverse, which is not overloaded -/ postfix [parsing-only] `⁻¹ᵉ`:std.prec.max_plus := inv section variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B} + -- The variant of mk' where f is explicit. + protected abbreviation mk := @is_equiv.mk' A B f + -- The identity function is an equivalence. - -- TODO: make A explicit - definition is_equiv_id : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp) + definition is_equiv_id (A : Type) : (@is_equiv A A id) := + is_equiv.mk id id (λa, idp) (λa, idp) (λa, idp) -- The composition of two equivalences is, again, an equivalence. definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (g ∘ f) := - is_equiv.mk ((inv f) ∘ (inv g)) + is_equiv.mk (g ∘ f) (f⁻¹ ∘ g⁻¹) (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c) (λa, ap (inv f) (sect g (f a)) ⬝ sect f a) (λa, (whisker_left _ (adj g (f a))) ⬝ @@ -92,7 +96,7 @@ namespace is_equiv ... = (ap f' (ap invf ff'a)⁻¹) ⬝ ap f' secta : by rewrite ap_inv ... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : by rewrite ap_con, eq3) in - is_equiv.mk (inv f) sect' retr' adj' + is_equiv.mk f' (inv f) sect' retr' adj' end section @@ -133,8 +137,7 @@ namespace is_equiv from eq_of_idp_eq_inv_con eq3, eq4) - definition adjointify : is_equiv f := - is_equiv.mk g ret adjointify_sect' adjointify_adj' + definition adjointify : is_equiv f := is_equiv.mk f g ret adjointify_sect' adjointify_adj' end @@ -213,7 +216,7 @@ namespace is_equiv --Transporting is an equivalence definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := - is_equiv.mk (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p) + is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p) end is_equiv diff --git a/hott/init/function.hlean b/hott/init/function.hlean index 803f1aea38..7675901cf6 100644 --- a/hott/init/function.hlean +++ b/hott/init/function.hlean @@ -13,7 +13,7 @@ import init.reserved_notation namespace function -variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} +variables {A B C D E : Type} definition compose [reducible] (f : B → C) (g : A → B) : A → C := λx, f (g x) @@ -44,8 +44,6 @@ precedence `∘'`:60 precedence `on`:1 precedence `$`:1 -variables {f g : A → B} - infixr ∘ := compose infixr ∘' := dcompose diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index dfa20c697a..e26ee1ca53 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -101,16 +101,15 @@ namespace is_trunc definition contr [H : is_contr A] (a : A) : !center = a := @contr_internal.contr A !is_trunc.to_internal a - --TODO: rename - definition center_eq [H : is_contr A] (x y : A) : x = y := + definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y := (contr x)⁻¹ ⬝ (contr y) definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q := - have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv), + have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv), (K p)⁻¹ ⬝ K q definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) := - is_contr.mk !center_eq (λ p, !hprop_eq_of_is_contr) + is_contr.mk !eq_of_is_contr (λ p, !hprop_eq_of_is_contr) local attribute is_contr_eq [instance] /- truncation is upward close -/ @@ -236,7 +235,7 @@ namespace is_trunc definition is_equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : is_equiv f := - is_equiv.mk g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim) + is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim) definition equiv_of_is_hprop [HA : is_hprop A] [HB : is_hprop B] (f : A → B) (g : B → A) : A ≃ B := @@ -252,11 +251,10 @@ namespace is_trunc open equiv -- A contractible type is equivalent to [Unit]. *) definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit := - equiv.mk (λ (x : A), ⋆) - (is_equiv.mk (λ (u : unit), center A) - (λ (u : unit), unit.rec_on u idp) - (λ (x : A), contr x) - (λ (x : A), !ap_constant⁻¹)) + equiv.MK (λ (x : A), ⋆) + (λ (u : unit), center A) + (λ (u : unit), unit.rec_on u idp) + (λ (x : A), contr x) -- TODO: port "Truncated morphisms" diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index ce45af0060..0ea744240c 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -137,7 +137,7 @@ namespace eq /- Path operations are equivalences -/ definition is_equiv_eq_inverse (a1 a2 : A) : is_equiv (@inverse A a1 a2) := - is_equiv.mk inverse inv_inv inv_inv (λp, eq.rec_on p idp) + is_equiv.mk inverse inverse inv_inv inv_inv (λp, eq.rec_on p idp) local attribute is_equiv_eq_inverse [instance] definition eq_equiv_eq_symm (a1 a2 : A) : (a1 = a2) ≃ (a2 = a1) := @@ -145,7 +145,7 @@ namespace eq definition is_equiv_concat_left [instance] (p : a1 = a2) (a3 : A) : is_equiv (@concat _ a1 a2 a3 p) := - is_equiv.mk (concat p⁻¹) + is_equiv.mk (concat p) (concat p⁻¹) (con_inv_cancel_left p) (inv_con_cancel_left p) (eq.rec_on p (λq, eq.rec_on q idp)) @@ -156,7 +156,7 @@ namespace eq definition is_equiv_concat_right [instance] (p : a2 = a3) (a1 : A) : is_equiv (λq : a1 = a2, q ⬝ p) := - is_equiv.mk (λq, q ⬝ p⁻¹) + is_equiv.mk (λq, q ⬝ p) (λq, q ⬝ p⁻¹) (λq, inv_con_cancel_right q p) (λq, con_inv_cancel_right q p) (eq.rec_on p (λq, eq.rec_on q idp)) diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 3322cdd587..92fa528fd0 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -60,7 +60,7 @@ namespace is_equiv protected definition sigma_char : (is_equiv f) ≃ (Σ(g : B → A) (ε : f ∘ g ∼ id) (η : g ∘ f ∼ id), Π(a : A), ε (f a) = ap f (η a)) := equiv.MK (λH, ⟨inv f, retr f, sect f, adj f⟩) - (λp, is_equiv.mk p.1 p.2.1 p.2.2.1 p.2.2.2) + (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2) (λp, begin cases p with [p1, p2], cases p2 with [p21, p22],