From 540d451e016d704497e80d57212ace52f690a943 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 7 Mar 2017 22:49:06 -0500 Subject: [PATCH] fix(hott): small fixes --- .../algebra/category/constructions/rezk.hlean | 46 +++++++++---------- hott/algebra/default.hlean | 2 +- hott/cubical/cube.hlean | 17 +++---- hott/cubical/square.hlean | 8 ++-- hott/hit/pushout.hlean | 8 ++-- hott/homotopy/wedge.hlean | 2 +- hott/init/pointed.hlean | 1 + hott/init/trunc.hlean | 2 +- hott/types/eq.hlean | 34 +++++++------- hott/types/pointed.hlean | 4 +- hott/types/sum.hlean | 2 +- src/emacs/lean-input.el | 1 + 12 files changed, 65 insertions(+), 62 deletions(-) diff --git a/hott/algebra/category/constructions/rezk.hlean b/hott/algebra/category/constructions/rezk.hlean index bd3e4ec13..b0d987668 100644 --- a/hott/algebra/category/constructions/rezk.hlean +++ b/hott/algebra/category/constructions/rezk.hlean @@ -7,13 +7,13 @@ Authors: Jakob von Raumer The Rezk completion -/ -import algebra.category hit.two_quotient types.trunc types.arrow algebra.category.functor.attributes +import hit.two_quotient types.trunc types.arrow algebra.category.functor.exponential_laws open eq category equiv trunc_two_quotient is_trunc iso e_closure function pi trunctype namespace rezk section - + universes l k parameters {A : Type.{l}} [C : precategory.{l k} A] include C @@ -57,7 +57,7 @@ namespace rezk (Pe : Π a, P (elt a)) (Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a =[pth f] Pe b) (Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b), change_path (resp_comp g f) (Pp (f ⬝i g)) = Pp f ⬝o Pp g) : P x := - rec Pe Pp Pcomp x + rec Pe Pp Pcomp x protected definition set_rec {P : rezk_carrier → Type} [Π x, is_set (P x)] (Pe : Π a, P (elt a)) (Pp : Π⦃a b⦄ (f : a ≅ b), Pe a =[pth f] Pe b) @@ -68,7 +68,7 @@ namespace rezk (Pe : Π a, P (elt a)) (x : rezk_carrier) : P x := rec Pe !center !center x - protected definition elim {P : Type} [is_trunc 1 P] (Pe : A → P) + protected definition elim {P : Type} [is_trunc 1 P] (Pe : A → P) (Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a = Pe b) (Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b), Pp (f ⬝i g) = Pp f ⬝ Pp g) (x : rezk_carrier) : P := @@ -79,7 +79,7 @@ namespace rezk { induction q with a b c g f, exact Pcomp g f } end - protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : rezk_carrier) + protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : rezk_carrier) (Pe : A → P) (Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a = Pe b) (Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b), Pp (f ⬝i g) = Pp f ⬝ Pp g) : P := elim Pe Pp Pcomp x @@ -157,9 +157,9 @@ namespace rezk --induction b using rezk.rec with b' b' b g, --why does this not work if it works below? refine @rezk.rec _ _ _ (rezk_hom_left_pth_1_trunc a a' f) _ _ _ b, intro b, apply equiv_precompose (to_hom f⁻¹ⁱ), --how do i unfold properly at this point? - { intro b b' g, apply equiv_pathover, intro g' g'' H, + { intro b b' g, apply equiv_pathover, intro g' g'' H, refine !pathover_rezk_hom_left_pt ⬝op _, - refine !assoc ⬝ ap (λ x, x ∘ _) _, refine eq_of_parallel_po_right _ H, + refine !assoc ⬝ ap (λ x, x ∘ _) _, refine eq_of_parallel_po_right _ H, apply pathover_rezk_hom_left_pt }, intro b b' b'' g g', apply @is_prop.elim, apply is_trunc_pathover, apply is_trunc_equiv end @@ -211,8 +211,8 @@ namespace rezk induction c using rezk.set_rec with c c c' ic, exact g ∘ f, { apply arrow_pathover_left, intro d, - apply concato !pathover_rezk_hom_left_pt, apply pathover_idp_of_eq, - apply concat, apply assoc, apply ap (λ x, x ∘ f), + apply concato !pathover_rezk_hom_left_pt, apply pathover_idp_of_eq, + apply concat, apply assoc, apply ap (λ x, x ∘ f), apply inverse, apply tr_eq_of_pathover, apply pathover_rezk_hom_left_pt }, end @@ -223,13 +223,13 @@ namespace rezk apply arrow_pathover_left, intro x, apply arrow_pathover_left, intro y, induction c using rezk.set_rec with c c c' ic, - { apply pathover_of_eq, apply inverse, + { apply pathover_of_eq, apply inverse, apply concat, apply ap (λ x, rezk_comp_pt_pt x _), apply tr_eq_of_pathover, apply pathover_rezk_hom_left, apply concat, apply ap (rezk_comp_pt_pt _), apply tr_eq_of_pathover, apply pathover_rezk_hom_left_pt, - refine !assoc ⬝ ap (λ x, x ∘ y) _, - refine !assoc⁻¹ ⬝ _, + refine !assoc ⬝ ap (λ x, x ∘ y) _, + refine !assoc⁻¹ ⬝ _, refine ap (λ y, x ∘ y) !iso.left_inverse ⬝ _, apply id_right }, apply @is_prop.elimo @@ -241,8 +241,8 @@ namespace rezk induction a using rezk.set_rec with a a a' ia, { induction b using rezk.set_rec with b b b' ib, apply rezk_comp_pt_pt g f, apply rezk_comp_pt_pth }, - { induction b using rezk.set_rec with b b b' ib, - apply arrow_pathover_left, intro f, + { induction b using rezk.set_rec with b b b' ib, + apply arrow_pathover_left, intro f, induction c using rezk.set_rec with c c c' ic, { apply concato, apply pathover_rezk_hom_left, apply pathover_idp_of_eq, refine !assoc⁻¹ ⬝ ap (λ x, g ∘ x) _⁻¹, @@ -291,7 +291,7 @@ namespace rezk intro C, apply Precategory.mk (@rezk_carrier (Precategory.carrier C) C), apply rezk_precategory _ _, end - + definition rezk_functor [constructor] (C : Precategory) : functor C (to_rezk_Precategory C) := begin fapply functor.mk, apply elt, @@ -337,7 +337,7 @@ namespace rezk (p : a = a') : to_hom (transport (λ x, iso x b) p f) = transport (λ x, hom _ _) p (to_hom f) := by cases p; reflexivity - private definition pathover_iso_pth {a b b' : A} (f : elt a ≅ elt b) + private definition pathover_iso_pth {a b b' : A} (f : elt a ≅ elt b) (ib : b ≅ b') : pathover (λ x, iso (elt a) x) f (pth ib) (f ⬝i elt_iso_of_iso ib) := begin apply pathover_of_tr_eq, apply iso_eq, @@ -361,9 +361,9 @@ namespace rezk apply pth, apply iso_of_elt_iso f, apply arrow_pathover, intro f g p, apply eq_pathover, refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹, apply square_of_eq, - refine !resp_comp⁻¹ ⬝ (ap pth _)⁻¹ ⬝ !idp_con⁻¹, - apply concat, apply inverse, apply ap rezk.iso_of_elt_iso, - apply eq_of_parallel_po_right (pathover_iso_pth _ _) p, + refine !resp_comp⁻¹ ⬝ (ap pth _)⁻¹ ⬝ !idp_con⁻¹, + apply concat, apply inverse, apply ap rezk.iso_of_elt_iso, + apply eq_of_parallel_po_right (pathover_iso_pth _ _) p, apply concat, apply iso_of_elt_iso_distrib, apply ap (λ x, _ ⬝i x), apply equiv.to_left_inv !iso_equiv_elt_iso end @@ -377,12 +377,12 @@ namespace rezk { induction b using rezk.set_rec with b b b' ib, { apply arrow_pathover, intro f g p, apply eq_pathover, refine !ap_id ⬝ph _ ⬝hp !ap_constant⁻¹, apply square_of_eq, - refine (ap pth _) ⬝ !resp_comp, + refine (ap pth _) ⬝ !resp_comp, assert H : g = (elt_iso_of_iso (iso.symm ia) ⬝i f), apply eq_of_parallel_po_right p (pathover_iso_pth' _ _), - rewrite H, apply inverse, + rewrite H, apply inverse, apply concat, apply ap (λ x, ia ⬝i x), apply iso_of_elt_iso_distrib, - apply concat, apply ap (λ x, _ ⬝i (x ⬝i _)), apply equiv.to_left_inv !iso_equiv_elt_iso, + apply concat, apply ap (λ x, _ ⬝i (x ⬝i _)), apply equiv.to_left_inv !iso_equiv_elt_iso, apply iso_eq, apply inverse_comp_cancel_right }, apply @is_prop.elimo } end @@ -437,5 +437,5 @@ namespace rezk prod.mk (fully_faithful_rezk_functor C) (essentially_surj_rezk_functor C) end - + end rezk diff --git a/hott/algebra/default.hlean b/hott/algebra/default.hlean index ab1f32887..c12af809b 100644 --- a/hott/algebra/default.hlean +++ b/hott/algebra/default.hlean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import .homotopy_group .ordered_field +import .homotopy_group .ordered_field .lattice diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean index 67a288031..c213e1778 100644 --- a/hott/cubical/cube.hlean +++ b/hott/cubical/cube.hlean @@ -30,12 +30,12 @@ namespace eq {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂} {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂} {p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂} - {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} - {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} {s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁} {s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁} {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁} {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁} + {s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} + {s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂} {b₁ b₂ b₃ b₄ : B} (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) @@ -126,6 +126,7 @@ namespace eq /- Transporting along a square -/ + -- TODO: remove: they are defined again below definition cube_transport110 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀} (p : s₁₁₀ = s₁₁₀') (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀' s₁₁₂ := @@ -339,11 +340,11 @@ namespace eq infix ` ⬝1 `:75 := cube_concat1 infix ` ⬝2 `:75 := cube_concat2 infix ` ⬝3 `:75 := cube_concat3 - infix ` ⬝p1 `:75 := eq_concat1 - infix ` ⬝1p `:75 := concat1_eq - infix ` ⬝p2 `:75 := eq_concat3 - infix ` ⬝2p `:75 := concat2_eq - infix ` ⬝p3 `:75 := eq_concat3 - infix ` ⬝3p `:75 := concat3_eq + infixr ` ⬝p1 `:75 := eq_concat1 + infixl ` ⬝1p `:75 := concat1_eq + infixr ` ⬝p2 `:75 := eq_concat2 + infixl ` ⬝2p `:75 := concat2_eq + infixr ` ⬝p3 `:75 := eq_concat3 + infixl ` ⬝3p `:75 := concat3_eq end eq diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index a182181f3..328908ef6 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -88,10 +88,10 @@ namespace eq infix ` ⬝h `:69 := hconcat --type using \tr infix ` ⬝v `:70 := vconcat --type using \tr - infix ` ⬝hp `:71 := hconcat_eq --type using \tr - infix ` ⬝vp `:73 := vconcat_eq --type using \tr - infix ` ⬝ph `:72 := eq_hconcat --type using \tr - infix ` ⬝pv `:74 := eq_vconcat --type using \tr + infixl ` ⬝hp `:71 := hconcat_eq --type using \tr + infixl ` ⬝vp `:73 := vconcat_eq --type using \tr + infixr ` ⬝ph `:72 := eq_hconcat --type using \tr + infixr ` ⬝pv `:74 := eq_vconcat --type using \tr postfix `⁻¹ʰ`:(max+1) := hinverse --type using \-1h postfix `⁻¹ᵛ`:(max+1) := vinverse --type using \-1v diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index aed77cceb..fc99321ed 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -206,7 +206,7 @@ namespace pushout krewrite [elim_glue, ap_inv, elim_glue, inv_inv], apply hrfl end - protected definition symm : pushout f g ≃ pushout g f := + protected definition symm [constructor] : pushout f g ≃ pushout g f := begin fapply equiv.MK, do 2 exact !pushout.transpose, do 2 (intro x; apply pushout.transpose_involutive), @@ -234,7 +234,7 @@ namespace pushout (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) include fh gh - protected definition functor [reducible] : pushout f g → pushout f' g' := + protected definition functor [reducible] [unfold 16] : pushout f g → pushout f' g' := begin intro x, induction x with a b z, { exact inl (bl a) }, @@ -254,7 +254,7 @@ namespace pushout include ietl iebl ietr open equiv is_equiv arrow - protected definition is_equiv_functor [instance] + protected definition is_equiv_functor [instance] [constructor] : is_equiv (pushout.functor tl bl tr fh gh) := adjointify (pushout.functor tl bl tr fh gh) @@ -336,7 +336,7 @@ namespace pushout (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl) include fh gh - protected definition equiv : pushout f g ≃ pushout f' g' := + protected definition equiv [constructor] : pushout f g ≃ pushout f' g' := equiv.mk (pushout.functor tl bl tr fh gh) _ end diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 6f4891f9e..ba1e73490 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -11,7 +11,7 @@ open eq pushout pointed unit trunc_index definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B) local attribute wedge [reducible] -definition pwedge (A B : Type*) : Type* := pointed.mk' (wedge A B) +definition pwedge [constructor] (A B : Type*) : Type* := pointed.mk' (wedge A B) infixr ` ∨ ` := pwedge namespace wedge diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index 256b5b767..ecedb0e92 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -88,6 +88,7 @@ structure ppi (A : Type*) (P : A → Type*) := (to_fun : Π a : A, P a) (resp_pt : to_fun (Point A) = Point (P (Point A))) +-- We could try to define pmap as a special case of ppi -- definition pmap (A B : Type*) := @ppi A (λa, B) structure pmap (A B : Type*) := (to_fun : A → B) diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 4b5ebb4e4..a86e4bdc7 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -325,7 +325,7 @@ namespace is_trunc open equiv /- A contractible type is equivalent to unit. -/ variable (A) - definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit := + definition equiv_unit_of_is_contr [constructor] [H : is_contr A] : A ≃ unit := equiv.MK (λ (x : A), ⋆) (λ (u : unit), center A) (λ (u : unit), unit.rec_on u idp) diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 2178c2d1c..1519ec50b 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -21,73 +21,73 @@ namespace eq /- some lemmas about whiskering or other higher paths -/ - theorem whisker_left_con_right (p : a₁ = a₂) {q q' q'' : a₂ = a₃} (r : q = q') (s : q' = q'') + definition whisker_left_con_right (p : a₁ = a₂) {q q' q'' : a₂ = a₃} (r : q = q') (s : q' = q'') : whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s := begin induction p, induction r, induction s, reflexivity end - theorem whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'') + definition whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'') : whisker_right q (r ⬝ s) = whisker_right q r ⬝ whisker_right q s := begin induction q, induction r, induction s, reflexivity end - theorem whisker_left_con_left (p : a₁ = a₂) (p' : a₂ = a₃) {q q' : a₃ = a₄} (r : q = q') + definition whisker_left_con_left (p : a₁ = a₂) (p' : a₂ = a₃) {q q' : a₃ = a₄} (r : q = q') : whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' := begin induction p', induction p, induction r, induction q, reflexivity end - theorem whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p') + definition whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p') : whisker_right (q ⬝ q') r = !con.assoc' ⬝ whisker_right q' (whisker_right q r) ⬝ !con.assoc := begin induction q', induction q, induction r, induction p, reflexivity end - theorem whisker_left_inv_left (p : a₂ = a₁) {q q' : a₂ = a₃} (r : q = q') + definition whisker_left_inv_left (p : a₂ = a₁) {q q' : a₂ = a₃} (r : q = q') : !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r := begin induction p, induction r, induction q, reflexivity end - theorem whisker_left_inv (p : a₁ = a₂) {q q' : a₂ = a₃} (r : q = q') + definition whisker_left_inv (p : a₁ = a₂) {q q' : a₂ = a₃} (r : q = q') : whisker_left p r⁻¹ = (whisker_left p r)⁻¹ := by induction r; reflexivity - theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p') + definition whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p') : whisker_right q r⁻¹ = (whisker_right q r)⁻¹ := by induction r; reflexivity - theorem ap_eq_apd10 {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) : + definition ap_eq_apd10 [unfold 5] {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) : ap (λh, h a) p = apd10 p a := by induction p; reflexivity - theorem inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p := + definition inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p := by induction r;induction p;reflexivity - theorem inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p := + definition inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p := by induction r;induction p;reflexivity - theorem ap_con_right_inv (f : A → B) (p : a₁ = a₂) + definition ap_con_right_inv (f : A → B) (p : a₁ = a₂) : ap_con f p p⁻¹ ⬝ whisker_left _ (ap_inv f p) ⬝ con.right_inv (ap f p) = ap (ap f) (con.right_inv p) := by induction p;reflexivity - theorem ap_con_left_inv (f : A → B) (p : a₁ = a₂) + definition ap_con_left_inv (f : A → B) (p : a₁ = a₂) : ap_con f p⁻¹ p ⬝ whisker_right _ (ap_inv f p) ⬝ con.left_inv (ap f p) = ap (ap f) (con.left_inv p) := by induction p;reflexivity - theorem idp_con_whisker_left {q q' : a₂ = a₃} (r : q = q') : + definition idp_con_whisker_left {q q' : a₂ = a₃} (r : q = q') : !idp_con⁻¹ ⬝ whisker_left idp r = r ⬝ !idp_con⁻¹ := by induction r;induction q;reflexivity - theorem whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') : + definition whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') : whisker_left idp r ⬝ !idp_con = !idp_con ⬝ r := by induction r;induction q;reflexivity - theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q := + definition idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q := by cases q;reflexivity definition ap_is_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b) @@ -105,13 +105,13 @@ namespace eq : (r₁ ◾ r₂)⁻¹ = r₁⁻¹ ◾ r₂⁻¹ := by induction r₁;induction r₂;reflexivity - theorem eq_con_inv_of_con_eq_whisker_left {A : Type} {a a₂ a₃ : A} + definition eq_con_inv_of_con_eq_whisker_left {A : Type} {a a₂ a₃ : A} {p : a = a₂} {q q' : a₂ = a₃} {r : a = a₃} (s' : q = q') (s : p ⬝ q' = r) : eq_con_inv_of_con_eq (whisker_left p s' ⬝ s) = eq_con_inv_of_con_eq s ⬝ whisker_left r (inverse2 s')⁻¹ := by induction s';induction q;induction s;reflexivity - theorem right_inv_eq_idp {A : Type} {a : A} {p : a = a} (r : p = idpath a) : + definition right_inv_eq_idp {A : Type} {a : A} {p : a = a} (r : p = idpath a) : con.right_inv p = r ◾ inverse2 r := by cases r;reflexivity diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 4997fb26b..23c69b07d 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -305,7 +305,7 @@ namespace pointed { apply idp_con} end - protected definition phomotopy.rfl [constructor] {f : A →* B} : f ~* f := + protected definition phomotopy.rfl [constructor] [reducible] {f : A →* B} : f ~* f := phomotopy.refl f protected definition phomotopy.trans [constructor] [trans] (p : f ~* g) (q : g ~* h) @@ -782,7 +782,7 @@ namespace pointed (p : h ~* f⁻¹ᵉ* ∘* g) : f ∘* h ~* g := (phomotopy_of_pinv_left_phomotopy p⁻¹*)⁻¹* - definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (p : f ~* f') (q : g ~* g') : + definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') : g ∘* f ~* g' ∘* f' := pwhisker_right f q ⬝* pwhisker_left g' p diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index cf43ac59a..da49a0043 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -116,7 +116,7 @@ namespace sum /- Equivalences -/ - definition is_equiv_sum_functor [constructor] [Hf : is_equiv f] [Hg : is_equiv g] + definition is_equiv_sum_functor [constructor] [instance] [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (sum_functor f g) := adjointify (sum_functor f g) (sum_functor f⁻¹ g⁻¹) diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index efc3ddfbc..0f7bfc5aa 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -356,6 +356,7 @@ order for the change to take effect." ("-1s" . ("⁻¹ˢ")) ("-1v" . ("⁻¹ᵛ")) ("-1E" . ("⁻¹ᴱ")) + ("-1hty" . ("⁻¹ʰᵗʸ")) ("-2" . ("⁻²" "₋₂")) ("-2o" . ("⁻²ᵒ")) ("-3" . ("⁻³"))