From e87a27cb4ba1629d106792ff156ce0909c8c0930 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 24 Nov 2016 00:13:05 -0500 Subject: [PATCH] fix(hott/init/path): reorder arguments of whisker_right --- hott/algebra/bundled.hlean | 38 ++++++------ hott/algebra/e_closure.hlean | 2 +- hott/algebra/group.hlean | 26 ++++---- hott/algebra/group_theory.hlean | 26 ++++---- hott/algebra/homotopy_group.hlean | 12 ++-- hott/algebra/ordered_group.hlean | 70 +++++++++++----------- hott/algebra/ordered_ring.hlean | 20 +++---- hott/algebra/ring.hlean | 26 ++++---- hott/algebra/trunc_group.hlean | 6 +- hott/cubical/square.hlean | 4 +- hott/eq2.hlean | 4 +- hott/hit/two_quotient.hlean | 1 + hott/homotopy/EM.hlean | 46 +++++++------- hott/homotopy/LES_of_homotopy_groups.hlean | 16 ++--- hott/homotopy/freudenthal.hlean | 4 +- hott/homotopy/homotopy_group.hlean | 2 +- hott/homotopy/smash.hlean | 8 +-- hott/init/equiv.hlean | 4 +- hott/init/path.hlean | 20 +++---- hott/types/arrow_2.hlean | 2 +- hott/types/eq.hlean | 10 ++-- hott/types/equiv.hlean | 6 +- hott/types/fin.hlean | 8 +-- hott/types/int/hott.hlean | 6 +- hott/types/pointed.hlean | 4 +- hott/types/trunc.hlean | 6 +- tests/lean/hott/614.hlean | 4 +- tests/lean/hott/615.hlean | 2 +- tests/lean/hott/beginend2.hlean | 2 +- tests/lean/hott/rewriter1.hlean | 4 +- tests/lean/hott/rw_binders.hlean | 2 +- 31 files changed, 196 insertions(+), 195 deletions(-) diff --git a/hott/algebra/bundled.hlean b/hott/algebra/bundled.hlean index cc1f436ad..e05ff916c 100644 --- a/hott/algebra/bundled.hlean +++ b/hott/algebra/bundled.hlean @@ -63,29 +63,29 @@ Group.struct G attribute AddGroup.struct Group.struct [instance] [priority 2000] -structure CommGroup := -(carrier : Type) (struct : comm_group carrier) +structure AbGroup := +(carrier : Type) (struct : ab_group carrier) -attribute CommGroup.carrier [coercion] +attribute AbGroup.carrier [coercion] -definition AddCommGroup : Type := CommGroup +definition AddAbGroup : Type := AbGroup -definition AddCommGroup.mk [constructor] [reducible] (G : Type) (H : add_comm_group G) : - AddCommGroup := -CommGroup.mk G H +definition AddAbGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_group G) : + AddAbGroup := +AbGroup.mk G H -definition AddCommGroup.struct [reducible] (G : AddCommGroup) : add_comm_group G := -CommGroup.struct G +definition AddAbGroup.struct [reducible] (G : AddAbGroup) : add_ab_group G := +AbGroup.struct G -attribute AddCommGroup.struct CommGroup.struct [instance] [priority 2000] +attribute AddAbGroup.struct AbGroup.struct [instance] [priority 2000] -definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := +definition Group_of_AbGroup [coercion] [constructor] (G : AbGroup) : Group := Group.mk G _ -attribute algebra._trans_of_Group_of_CommGroup_1 - algebra._trans_of_Group_of_CommGroup - algebra._trans_of_Group_of_CommGroup_3 [constructor] -attribute algebra._trans_of_Group_of_CommGroup_2 [unfold 1] +attribute algebra._trans_of_Group_of_AbGroup_1 + algebra._trans_of_Group_of_AbGroup + algebra._trans_of_Group_of_AbGroup_3 [constructor] +attribute algebra._trans_of_Group_of_AbGroup_2 [unfold 1] -- structure AddSemigroup := @@ -118,9 +118,9 @@ attribute algebra._trans_of_Group_of_CommGroup_2 [unfold 1] -- attribute AddGroup.carrier [coercion] -- attribute AddGroup.struct [instance] --- structure AddCommGroup := --- (carrier : Type) (struct : add_comm_group carrier) +-- structure AddAbGroup := +-- (carrier : Type) (struct : add_ab_group carrier) --- attribute AddCommGroup.carrier [coercion] --- attribute AddCommGroup.struct [instance] +-- attribute AddAbGroup.carrier [coercion] +-- attribute AddAbGroup.struct [instance] end algebra diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 2aa3cc3d4..36c32f475 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -158,7 +158,7 @@ section ap_e_closure_elim_h e p t = ap_e_closure_elim_h (λa a' s, ap g (e s)) (λa a' s, (ap_compose h g (e s))⁻¹ ⬝ p s) t := begin - refine whisker_right (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ _ ⬝ _, + refine whisker_right _ (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ ⬝ _, refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, apply eq_of_square, apply transpose, -- the rest of the proof is almost the same as the proof of ap_ap_e_closure_elim[_h]. diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index 2a0384baf..27fedf883 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -346,7 +346,7 @@ section group end group -structure comm_group [class] (A : Type) extends group A, comm_monoid A +structure ab_group [class] (A : Type) extends group A, comm_monoid A /- additive group -/ @@ -551,21 +551,21 @@ section add_group end add_group -definition add_comm_group [class] : Type → Type := comm_group +definition add_ab_group [class] : Type → Type := ab_group -definition add_group_of_add_comm_group [reducible] [trans_instance] (A : Type) - [H : add_comm_group A] : add_group A := -@comm_group.to_group A H +definition add_group_of_add_ab_group [reducible] [trans_instance] (A : Type) + [H : add_ab_group A] : add_group A := +@ab_group.to_group A H -definition add_comm_monoid_of_add_comm_group [reducible] [trans_instance] (A : Type) - [H : add_comm_group A] : add_comm_monoid A := -@comm_group.to_comm_monoid A H +definition add_comm_monoid_of_add_ab_group [reducible] [trans_instance] (A : Type) + [H : add_ab_group A] : add_comm_monoid A := +@ab_group.to_comm_monoid A H -definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A := s -definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A := s +definition add_ab_group.to_ab_group {A : Type} [s : add_ab_group A] : ab_group A := s +definition ab_group.to_add_ab_group {A : Type} [s : ab_group A] : add_ab_group A := s -section add_comm_group - variable [s : add_comm_group A] +section add_ab_group + variable [s : add_ab_group A] include s theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c := @@ -606,7 +606,7 @@ section add_comm_group theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b := by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub] -end add_comm_group +end add_ab_group definition group_of_add_group (A : Type) [G : add_group A] : group A := ⦃group, diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 3c3ad6e28..6e4f5eb2d 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -21,12 +21,12 @@ namespace group definition Group.struct' [instance] [reducible] (G : Group) : group G := Group.struct G - definition comm_group_Group_of_CommGroup [instance] [constructor] [priority 900] - (G : CommGroup) : comm_group (Group_of_CommGroup G) := + definition ab_group_Group_of_AbGroup [instance] [constructor] [priority 900] + (G : AbGroup) : ab_group (Group_of_AbGroup G) := begin esimp, exact _ end - definition comm_group_pSet_of_Group [instance] (G : CommGroup) : comm_group (pSet_of_Group G) := - CommGroup.struct G + definition ab_group_pSet_of_Group [instance] (G : AbGroup) : ab_group (pSet_of_Group G) := + AbGroup.struct G definition group_pSet_of_Group [instance] [priority 900] (G : Group) : group (pSet_of_Group G) := @@ -463,14 +463,14 @@ namespace group definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ := Group_eq (equiv_of_isomorphism φ) (respect_mul φ) - definition comm_group.to_has_mul {A : Type} (H : comm_group A) : has_mul A := _ - local attribute comm_group.to_has_mul [coercion] + definition ab_group.to_has_mul {A : Type} (H : ab_group A) : has_mul A := _ + local attribute ab_group.to_has_mul [coercion] - definition comm_group_eq {A : Type} {G H : comm_group A} + definition ab_group_eq {A : Type} {G H : ab_group A} (same_mul : Π(g h : A), @mul A G g h = @mul A H g h) : G = H := begin - have g_eq : @comm_group.to_group A G = @comm_group.to_group A H, from group_eq same_mul, + have g_eq : @ab_group.to_group A G = @ab_group.to_group A H, from group_eq same_mul, cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5, cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5, have pm : Gm = Hm, from ap (@mul _ ∘ group.to_has_mul) g_eq, @@ -487,18 +487,18 @@ namespace group reflexivity end - definition comm_group_pathover {A B : Type} {G : comm_group A} {H : comm_group B} {p : A = B} + definition ab_group_pathover {A B : Type} {G : ab_group A} {H : ab_group B} {p : A = B} (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H := begin induction p, - apply pathover_idp_of_eq, exact comm_group_eq (resp_mul) + apply pathover_idp_of_eq, exact ab_group_eq (resp_mul) end - definition CommGroup_eq_of_isomorphism {G₁ G₂ : CommGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := + definition AbGroup_eq_of_isomorphism {G₁ G₂ : AbGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := begin induction G₁, induction G₂, - apply apd011 CommGroup.mk (ua (equiv_of_isomorphism φ)), - apply comm_group_pathover, + apply apd011 AbGroup.mk (ua (equiv_of_isomorphism φ)), + apply ab_group_pathover, intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹ end diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 2f3afb165..2347493bf 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -26,18 +26,18 @@ namespace eq group (carrier (ptrunctype.to_pType (π[k + 1] A))) := group_homotopy_group k A - definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) - : comm_group (π[succ (succ n)] A) := - trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton + definition ab_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) + : ab_group (π[succ (succ n)] A) := + trunc_ab_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton - local attribute comm_group_homotopy_group [instance] + local attribute ab_group_homotopy_group [instance] definition ghomotopy_group [constructor] : Π(n : ℕ) [is_succ n] (A : Type*), Group | (succ n) x A := Group.mk (π[succ n] A) _ definition cghomotopy_group [constructor] : - Π(n : ℕ) [is_at_least_two n] (A : Type*), CommGroup - | (succ (succ n)) x A := CommGroup.mk (π[succ (succ n)] A) _ + Π(n : ℕ) [is_at_least_two n] (A : Type*), AbGroup + | (succ (succ n)) x A := AbGroup.mk (π[succ (succ n)] A) _ definition fundamental_group [constructor] (A : Type*) : Group := ghomotopy_group 1 A diff --git a/hott/algebra/ordered_group.hlean b/hott/algebra/ordered_group.hlean index 3507d6a66..1feba7a98 100644 --- a/hott/algebra/ordered_group.hlean +++ b/hott/algebra/ordered_group.hlean @@ -213,40 +213,40 @@ end /- partially ordered groups -/ -structure ordered_mul_comm_group [class] (A : Type) extends comm_group A, order_pair A := +structure ordered_mul_ab_group [class] (A : Type) extends ab_group A, order_pair A := (mul_le_mul_left : Πa b, le a b → Πc, le (mul c a) (mul c b)) (mul_lt_mul_left : Πa b, lt a b → Π c, lt (mul c a) (mul c b)) -definition ordered_comm_group [class] : Type → Type := ordered_mul_comm_group +definition ordered_ab_group [class] : Type → Type := ordered_mul_ab_group -definition add_comm_group_of_ordered_comm_group [reducible] [trans_instance] (A : Type) - [H : ordered_comm_group A] : add_comm_group A := -@ordered_mul_comm_group.to_comm_group A H +definition add_ab_group_of_ordered_ab_group [reducible] [trans_instance] (A : Type) + [H : ordered_ab_group A] : add_ab_group A := +@ordered_mul_ab_group.to_ab_group A H -theorem ordered_mul_comm_group.le_of_mul_le_mul_left [s : ordered_mul_comm_group A] {a b c : A} +theorem ordered_mul_ab_group.le_of_mul_le_mul_left [s : ordered_mul_ab_group A] {a b c : A} (H : a * b ≤ a * c) : b ≤ c := -have H' : a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_comm_group.mul_le_mul_left _ _ H _, +have H' : a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_ab_group.mul_le_mul_left _ _ H _, by rewrite *inv_mul_cancel_left at H'; exact H' -theorem ordered_mul_comm_group.lt_of_mul_lt_mul_left [s : ordered_mul_comm_group A] {a b c : A} +theorem ordered_mul_ab_group.lt_of_mul_lt_mul_left [s : ordered_mul_ab_group A] {a b c : A} (H : a * b < a * c) : b < c := -have H' : a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_comm_group.mul_lt_mul_left _ _ H _, +have H' : a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_ab_group.mul_lt_mul_left _ _ H _, by rewrite *inv_mul_cancel_left at H'; exact H' -definition ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid [reducible] [trans_instance] - [s : ordered_mul_comm_group A] : ordered_mul_cancel_comm_monoid A := +definition ordered_mul_ab_group.to_ordered_mul_cancel_comm_monoid [reducible] [trans_instance] + [s : ordered_mul_ab_group A] : ordered_mul_cancel_comm_monoid A := ⦃ ordered_mul_cancel_comm_monoid, s, mul_left_cancel := @mul.left_cancel A _, mul_right_cancel := @mul.right_cancel A _, - le_of_mul_le_mul_left := @ordered_mul_comm_group.le_of_mul_le_mul_left A _, - lt_of_mul_lt_mul_left := @ordered_mul_comm_group.lt_of_mul_lt_mul_left A _⦄ + le_of_mul_le_mul_left := @ordered_mul_ab_group.le_of_mul_le_mul_left A _, + lt_of_mul_lt_mul_left := @ordered_mul_ab_group.lt_of_mul_lt_mul_left A _⦄ -definition ordered_comm_group.to_ordered_cancel_comm_monoid [reducible] [trans_instance] - [s : ordered_comm_group A] : ordered_cancel_comm_monoid A := -@ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid A s +definition ordered_ab_group.to_ordered_cancel_comm_monoid [reducible] [trans_instance] + [s : ordered_ab_group A] : ordered_cancel_comm_monoid A := +@ordered_mul_ab_group.to_ordered_mul_cancel_comm_monoid A s section - variables [s : ordered_comm_group A] (a b c d e : A) + variables [s : ordered_ab_group A] (a b c d e : A) include s theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a := @@ -603,37 +603,37 @@ end /- linear ordered group with decidable order -/ -structure decidable_linear_ordered_mul_comm_group [class] (A : Type) - extends comm_group A, decidable_linear_order A := +structure decidable_linear_ordered_mul_ab_group [class] (A : Type) + extends ab_group A, decidable_linear_order A := (mul_le_mul_left : Π a b, le a b → Π c, le (mul c a) (mul c b)) (mul_lt_mul_left : Π a b, lt a b → Π c, lt (mul c a) (mul c b)) -definition decidable_linear_ordered_comm_group [class] : Type → Type := -decidable_linear_ordered_mul_comm_group +definition decidable_linear_ordered_ab_group [class] : Type → Type := +decidable_linear_ordered_mul_ab_group -definition add_comm_group_of_decidable_linear_ordered_comm_group [reducible] [trans_instance] (A : Type) - [H : decidable_linear_ordered_comm_group A] : add_comm_group A := -@decidable_linear_ordered_mul_comm_group.to_comm_group A H +definition add_ab_group_of_decidable_linear_ordered_ab_group [reducible] [trans_instance] (A : Type) + [H : decidable_linear_ordered_ab_group A] : add_ab_group A := +@decidable_linear_ordered_mul_ab_group.to_ab_group A H -definition decidable_linear_order_of_decidable_linear_ordered_comm_group [reducible] - [trans_instance] (A : Type) [H : decidable_linear_ordered_comm_group A] : +definition decidable_linear_order_of_decidable_linear_ordered_ab_group [reducible] + [trans_instance] (A : Type) [H : decidable_linear_ordered_ab_group A] : decidable_linear_order A := -@decidable_linear_ordered_mul_comm_group.to_decidable_linear_order A H +@decidable_linear_ordered_mul_ab_group.to_decidable_linear_order A H -definition decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group [reducible] - [trans_instance] (A : Type) [s : decidable_linear_ordered_mul_comm_group A] : - ordered_mul_comm_group A := -⦃ ordered_mul_comm_group, s, +definition decidable_linear_ordered_mul_ab_group.to_ordered_mul_ab_group [reducible] + [trans_instance] (A : Type) [s : decidable_linear_ordered_mul_ab_group A] : + ordered_mul_ab_group A := +⦃ ordered_mul_ab_group, s, le_of_lt := @le_of_lt A _, lt_of_le_of_lt := @lt_of_le_of_lt A _, lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄ -definition decidable_linear_ordered_comm_group.to_ordered_comm_group [reducible] [trans_instance] - (A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := -@decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group A s +definition decidable_linear_ordered_ab_group.to_ordered_ab_group [reducible] [trans_instance] + (A : Type) [s : decidable_linear_ordered_ab_group A] : ordered_ab_group A := +@decidable_linear_ordered_mul_ab_group.to_ordered_mul_ab_group A s section - variables [s : decidable_linear_ordered_comm_group A] + variables [s : decidable_linear_ordered_ab_group A] variables {a b c d e : A} include s diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean index 2d29ac3bd..2bb0c68e7 100644 --- a/hott/algebra/ordered_ring.hlean +++ b/hott/algebra/ordered_ring.hlean @@ -34,7 +34,7 @@ structure ordered_semiring (A : Type) -- ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/ attribute ordered_semiring [class] -definition add_comm_group_of_ordered_semiring [trans_instance] [reducible] (A : Type) +definition add_ab_group_of_ordered_semiring [trans_instance] [reducible] (A : Type) [H : ordered_semiring A] : semiring A := @ordered_semiring.to_semiring A H @@ -209,7 +209,7 @@ structure decidable_linear_ordered_semiring [class] (A : Type) /- ring structures -/ -structure ordered_ring (A : Type) extends ring A, ordered_mul_comm_group A renaming +structure ordered_ring (A : Type) extends ring A, ordered_mul_ab_group A renaming mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left mul_lt_mul_left→add_lt_add_left, @@ -218,16 +218,16 @@ structure ordered_ring (A : Type) extends ring A, ordered_mul_comm_group A renam (mul_pos : Πa b, lt zero a → lt zero b → lt zero (mul a b)) -- /- we make it a class now (and not as part of the structure) to avoid --- ordered_ring.to_ordered_mul_comm_group to be an instance -/ +-- ordered_ring.to_ordered_mul_ab_group to be an instance -/ attribute ordered_ring [class] -definition add_comm_group_of_ordered_ring [reducible] [trans_instance] (A : Type) +definition add_ab_group_of_ordered_ring [reducible] [trans_instance] (A : Type) [H : ordered_ring A] : ring A := @ordered_ring.to_ring A H definition monoid_of_ordered_ring [reducible] [trans_instance] (A : Type) - [H : ordered_ring A] : ordered_comm_group A := -@ordered_ring.to_ordered_mul_comm_group A H + [H : ordered_ring A] : ordered_ab_group A := +@ordered_ring.to_ordered_mul_ab_group A H definition zero_ne_one_class_of_ordered_ring [reducible] [trans_instance] (A : Type) [H : ordered_ring A] : zero_ne_one_class A := @@ -486,7 +486,7 @@ end Search on mult_le_cancel_right1 in Rings.thy. -/ structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A, - decidable_linear_ordered_mul_comm_group A renaming + decidable_linear_ordered_mul_ab_group A renaming mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left mul_lt_mul_left→add_lt_add_left @@ -500,10 +500,10 @@ definition linear_ordered_comm_ring_of_decidable_linear_ordered_comm_ring [reduc linear_ordered_comm_ring A := @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring A H -definition decidable_linear_ordered_comm_group_of_decidable_linear_ordered_comm_ring [reducible] +definition decidable_linear_ordered_ab_group_of_decidable_linear_ordered_comm_ring [reducible] [trans_instance] (A : Type) [H : decidable_linear_ordered_comm_ring A] : - decidable_linear_ordered_comm_group A := -@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_comm_group A H + decidable_linear_ordered_ab_group A := +@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_ab_group A H section variable [s : decidable_linear_ordered_comm_ring A] diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean index 05c23db07..a9242a5d6 100644 --- a/hott/algebra/ring.hlean +++ b/hott/algebra/ring.hlean @@ -186,17 +186,17 @@ end comm_semiring /- ring -/ -structure ring (A : Type) extends comm_group A renaming mul→add mul_assoc→add_assoc +structure ring (A : Type) extends ab_group A renaming mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm, monoid A, distrib A /- we make it a class now (and not as part of the structure) to avoid - ring.to_comm_group to be an instance -/ + ring.to_ab_group to be an instance -/ attribute ring [class] -definition add_comm_group_of_ring [reducible] [trans_instance] (A : Type) - [H : ring A] : add_comm_group A := -@ring.to_comm_group A H +definition add_ab_group_of_ring [reducible] [trans_instance] (A : Type) + [H : ring A] : add_ab_group A := +@ring.to_ab_group A H definition monoid_of_ring [reducible] [trans_instance] (A : Type) [H : ring A] : monoid A := @@ -485,7 +485,7 @@ theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b := theorem mk_eq (a : A) : a = a := rfl -theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) : +theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_ab_group A] (a b c : A) (H : c + a + b = 0) : -a + -b = c := begin apply add_neg_eq_of_eq_add, @@ -493,26 +493,26 @@ theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H] end -theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c := +theorem neg_add_neg_helper [s : add_ab_group A] (a b c : A) (H : a + b = c) : -a + -b = -c := begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end -theorem neg_add_pos_eq_of_eq_add [s : add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c := +theorem neg_add_pos_eq_of_eq_add [s : add_ab_group A] (a b c : A) (H : b = c + a) : -a + b = c := begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end -theorem neg_add_pos_helper1 [s : add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c := +theorem neg_add_pos_helper1 [s : add_ab_group A] (a b c : A) (H : b + c = a) : -a + b = -c := begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end -theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c := +theorem neg_add_pos_helper2 [s : add_ab_group A] (a b c : A) (H : a + c = b) : -a + b = c := begin apply neg_add_eq_of_eq_add, rewrite H end -theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c := +theorem pos_add_neg_helper [s : add_ab_group A] (a b c : A) (H : b + a = c) : a + b = c := by rewrite [add.comm, H] -theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) +theorem sub_eq_add_neg_helper [s : add_ab_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) (H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e := by rewrite [sub_eq_add_neg, H₁, H₂, H] -theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂) +theorem pos_add_pos_helper [s : add_ab_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂) (H : h₁ + h₂ = c) : a + b = c := by rewrite [H₁, H₂, H] diff --git a/hott/algebra/trunc_group.hlean b/hott/algebra/trunc_group.hlean index 9ea7e91fc..cdd85090a 100644 --- a/hott/algebra/trunc_group.hlean +++ b/hott/algebra/trunc_group.hlean @@ -96,9 +96,9 @@ namespace algebra mul_left_inv := algebra.trunc_mul_left_inv 0 mul_left_inv, is_set_carrier := _⦄ - definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) - : comm_group (trunc 0 A) := - ⦃comm_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄ + definition trunc_ab_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) + : ab_group (trunc 0 A) := + ⦃ab_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄ end end algebra diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 7621a9c94..5079e7938 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -378,11 +378,11 @@ namespace eq by induction r;induction p;reflexivity definition eq_of_square_eq_vconcat {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) - : eq_of_square (r ⬝pv s₁₁) = whisker_right r p₂₁ ⬝ eq_of_square s₁₁ := + : eq_of_square (r ⬝pv s₁₁) = whisker_right p₂₁ r ⬝ eq_of_square s₁₁ := by induction s₁₁;cases r;reflexivity definition eq_of_square_eq_hconcat {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) - : eq_of_square (r ⬝ph s₁₁) = eq_of_square s₁₁ ⬝ (whisker_right r p₁₂)⁻¹ := + : eq_of_square (r ⬝ph s₁₁) = eq_of_square s₁₁ ⬝ (whisker_right p₁₂ r)⁻¹ := by induction r;reflexivity definition eq_of_square_vconcat_eq {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 23e9a7445..1c04066a0 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -44,7 +44,7 @@ namespace eq theorem ap_con_left_inv_sq {A B : Type} {a1 a2 : A} (f : A → B) (p : a1 = a2) : square (ap (ap f) (con.left_inv p)) (con.left_inv (ap f p)) - (ap_con f p⁻¹ p ⬝ whisker_right (ap_inv f p) _) + (ap_con f p⁻¹ p ⬝ whisker_right _ (ap_inv f p)) idp := by cases p;apply vrefl @@ -91,7 +91,7 @@ namespace eq natural_square_tr (ap_compose g f) r theorem whisker_right_eq_of_con_inv_eq_idp {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) : - whisker_right (eq_of_con_inv_eq_idp r) q⁻¹ ⬝ con.right_inv q = r := + whisker_right q⁻¹ (eq_of_con_inv_eq_idp r) ⬝ con.right_inv q = r := by induction q; esimp at r; cases r; reflexivity theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 1aa6e2c8f..352031bf8 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -279,6 +279,7 @@ namespace simple_two_quotient ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) := !elim_eq_of_rel + local attribute whisker_right [reducible] protected theorem elim_incl2w {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index c3bce08bf..9ced6241f 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -192,7 +192,7 @@ end EM open hopf susp namespace EM /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/ - variables {G : CommGroup} (n : ℕ) + variables {G : AbGroup} (n : ℕ) definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G := begin @@ -260,7 +260,7 @@ namespace EM refine freudenthal_pequiv _ this } end - definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := + definition loopn_EMadd1_pequiv_EM1 (G : AbGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := begin induction n with n e, { reflexivity }, @@ -270,7 +270,7 @@ namespace EM end -- use loopn_EMadd1_pequiv_EM1 in this definition? - definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := + definition loopn_EMadd1 (G : AbGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := begin induction n with n e, { apply loop_EM1 }, @@ -279,15 +279,15 @@ namespace EM exact e } end - definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* + definition loopn_EMadd1_succ [unfold_full] (G : AbGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n := by reflexivity - definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + definition EM_up {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) : Ω[succ n] (Ω X) ≃* G := !loopn_succ_in⁻¹ᵉ* ⬝e* e - definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ} + definition is_homomorphism_EM_up {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q) (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q := @@ -295,7 +295,7 @@ namespace EM refine _ ⬝ !r, apply ap e, esimp, apply apn_con end - definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ) + definition EMadd1_pmap [unfold 8] {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) (r : Πp q, e (p ⬝ q) = e p * e q) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := @@ -307,12 +307,12 @@ namespace EM (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), end - definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) + definition EMadd1_pmap_succ {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r = ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := by reflexivity - definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) + definition loop_EMadd1_pmap {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) (r : Πp q, e (p ⬝ q) = e p * e q) [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~* @@ -329,7 +329,7 @@ namespace EM reflexivity } end - definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) + definition loopn_EMadd1_pmap' {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) (r : Πp q, e (p ⬝ q) = e p * e q) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* := @@ -346,7 +346,7 @@ namespace EM apply pinv_pcompose_cancel_left end - definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) + definition EMadd1_pequiv' {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := begin @@ -365,7 +365,7 @@ namespace EM do 2 exact trivial_homotopy_group_of_is_trunc _ H} end - definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) + definition EMadd1_pequiv {G : AbGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := begin have is_set (Ω[succ n] X), from !is_set_loopn, @@ -373,7 +373,7 @@ namespace EM intro p q, esimp, exact to_respect_mul e (tr p) (tr q) end - definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) + definition EMadd1_pequiv_succ {G : AbGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X := EMadd1_pequiv (succ n) e @@ -389,7 +389,7 @@ namespace EM EMadd1_pequiv_succ n !isomorphism.refl /- K(G, n) -/ - definition EM (G : CommGroup) : ℕ → Type* + definition EM (G : AbGroup) : ℕ → Type* | 0 := G | (k+1) := EMadd1 G k @@ -449,7 +449,7 @@ namespace EM { reflexivity } end - definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + definition EMadd1_functor [constructor] {G H : AbGroup} (φ : G →g H) (n : ℕ) : EMadd1 G n →* EMadd1 H n := begin induction n with n ψ, @@ -457,7 +457,7 @@ namespace EM { apply ptrunc_functor, apply psusp_functor, exact ψ } end - definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : + definition EM_functor [unfold 4] {G H : AbGroup} (φ : G →g H) (n : ℕ) : K G n →* K H n := begin cases n with n, @@ -481,7 +481,7 @@ namespace EM begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end - /- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ + /- Equivalence of AbGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ open trunc_index definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n]) @@ -497,16 +497,16 @@ namespace EM EMadd1 (πag[n+2] X) (succ n) ≃* X := EMadd1_pequiv_type X n - definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : - CommGroup ≃ (n + 1 + 1)-Type*[n+1] := + definition AbGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : + AbGroup ≃ (n + 1 + 1)-Type*[n+1] := equiv.MK (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _) (λX, πag[n+2] X) begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end - begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end + begin intro G, apply AbGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end - definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) : - CommGroup ≃ (n.+2)-Type*[n.+1] := - CommGroup_equiv_ptruncconntype' n + definition AbGroup_equiv_ptruncconntype [constructor] (n : ℕ) : + AbGroup ≃ (n.+2)-Type*[n.+1] := + AbGroup_equiv_ptruncconntype' n end EM diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 6fc10effd..b3c1a290f 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -716,20 +716,20 @@ namespace chain_complex | (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition comm_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), - comm_group (LES_of_homotopy_groups (n + 2, x)) - | (fin.mk 0 H) := proof comm_group_homotopy_group n Y qed - | (fin.mk 1 H) := proof comm_group_homotopy_group n X qed - | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed + definition ab_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), + ab_group (LES_of_homotopy_groups (n + 2, x)) + | (fin.mk 0 H) := proof ab_group_homotopy_group n Y qed + | (fin.mk 1 H) := proof ab_group_homotopy_group n X qed + | (fin.mk 2 H) := proof ab_group_homotopy_group n (pfiber f) qed | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) - definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} := - CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) - (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) + definition AbGroup_LES_of_homotopy_groups (n : +3ℕ) : AbGroup.{u} := + AbGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) + (ab_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ), Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k diff --git a/hott/homotopy/freudenthal.hlean b/hott/homotopy/freudenthal.hlean index ba74bad2d..07329ef14 100644 --- a/hott/homotopy/freudenthal.hlean +++ b/hott/homotopy/freudenthal.hlean @@ -110,7 +110,7 @@ namespace freudenthal section apply trunc_pathover, apply eq_pathover_constant_left_id_right, apply square_of_eq, - exact whisker_right !con.right_inv (merid a) + exact whisker_right (merid a) !con.right_inv end definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) := @@ -122,7 +122,7 @@ namespace freudenthal section end definition decode_coh_lem {A : Type} {a a' : A} (p : a = a') - : whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ := + : whisker_right p (con.right_inv p) = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ := by induction p; reflexivity theorem decode_coh (a : A) : decode_north =[merid a] decode_south := diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index d6953bfc1..673260167 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -63,7 +63,7 @@ namespace is_trunc end /- Corollaries of the LES of homotopy groups -/ - local attribute comm_group.to_group [coercion] + local attribute ab_group.to_group [coercion] local attribute is_equiv_tinverse [instance] open prod chain_complex group fin equiv function is_equiv lift diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean index a5b4ea2b8..058663728 100644 --- a/hott/homotopy/smash.hlean +++ b/hott/homotopy/smash.hlean @@ -50,7 +50,7 @@ namespace smash gluel' a pt ⬝ gluer' pt b definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b := - whisker_right !con.right_inv _ ⬝ !idp_con + whisker_right _ !con.right_inv ⬝ !idp_con definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt := proof whisker_left _ !con.right_inv qed @@ -82,11 +82,11 @@ namespace smash { exact gluel pt ▸ Pmk pt pt }, { exact gluer pt ▸ Pmk pt pt }, { refine change_path _ (Pg a pt ⬝o !pathover_tr), - refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _, + refine whisker_right _ !glue_pt_right ⬝ _, esimp, refine !con.assoc ⬝ _, apply whisker_left, apply con.left_inv }, { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr), - refine whisker_right !glue_pt_left⁻² _ ⬝ _, - refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _, + refine whisker_right _ !glue_pt_left⁻² ⬝ _, + refine whisker_right _ !inv_con_inv_right ⬝ _, refine !con.assoc ⬝ _, apply whisker_left, apply con.left_inv } end diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index d3c4cc471..7c68fe2d8 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -174,12 +174,12 @@ namespace is_equiv (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := - !ap_con ⬝ whisker_right !ap_con _ + !ap_con ⬝ whisker_right _ !ap_con ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) ◾ (inverse (ap_compose f f⁻¹ _)) ◾ (adj f _)⁻¹) ⬝ con_ap_con_eq_con_con (right_inv f) _ _ - ⬝ whisker_right !con.left_inv _ + ⬝ whisker_right _ !con.left_inv ⬝ !idp_con definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q := diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 0173ea6ba..727d4e48e 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -631,7 +631,7 @@ namespace eq definition whisker_left [unfold 8] (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r := idp ◾ h - definition whisker_right [unfold 7] {p q : x = y} (h : p = q) (r : y = z) : p ⬝ r = q ⬝ r := + definition whisker_right [unfold 7] {p q : x = y} (r : y = z) (h : p = q) : p ⬝ r = q ⬝ r := h ◾ idp -- Unwhiskering, a.k.a. cancelling @@ -640,16 +640,16 @@ namespace eq λs, !inv_con_cancel_left⁻¹ ⬝ whisker_left p⁻¹ s ⬝ !inv_con_cancel_left definition cancel_right {x y z : A} {p q : x = y} (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) := - λs, !con_inv_cancel_right⁻¹ ⬝ whisker_right s r⁻¹ ⬝ !con_inv_cancel_right + λs, !con_inv_cancel_right⁻¹ ⬝ whisker_right r⁻¹ s ⬝ !con_inv_cancel_right -- Whiskering and identity paths. definition whisker_right_idp {p q : x = y} (h : p = q) : - whisker_right h idp = h := + whisker_right idp h = h := by induction h; induction p; reflexivity definition whisker_right_idp_left [unfold_full] (p : x = y) (q : y = z) : - whisker_right idp q = idp :> (p ⬝ q = p ⬝ q) := + whisker_right q idp = idp :> (p ⬝ q = p ⬝ q) := idp definition whisker_left_idp_right [unfold_full] (p : x = y) (q : y = z) : @@ -668,7 +668,7 @@ namespace eq end definition con2_idp [unfold_full] {p q : x = y} (h : p = q) : - h ◾ idp = whisker_right h idp :> (p ⬝ idp = q ⬝ idp) := + h ◾ idp = whisker_right idp h :> (p ⬝ idp = q ⬝ idp) := idp definition idp_con2 [unfold_full] {p q : x = y} (h : p = q) : @@ -686,16 +686,16 @@ namespace eq by induction d; induction c; induction b;induction a; reflexivity definition con2_eq_rl {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z} - (a : p = p') (b : q = q') : a ◾ b = whisker_right a q ⬝ whisker_left p' b := + (a : p = p') (b : q = q') : a ◾ b = whisker_right q a ⬝ whisker_left p' b := by induction b; induction a; reflexivity definition con2_eq_lf {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z} - (a : p = p') (b : q = q') : a ◾ b = whisker_left p b ⬝ whisker_right a q' := + (a : p = p') (b : q = q') : a ◾ b = whisker_left p b ⬝ whisker_right q' a := by induction b; induction a; reflexivity definition whisker_right_con_whisker_left {x y z : A} {p p' : x = y} {q q' : y = z} (a : p = p') (b : q = q') : - (whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') := + (whisker_right q a) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right q' a) := by induction b; induction a; reflexivity -- Structure corresponding to the coherence equations of a bicategory. @@ -704,13 +704,13 @@ namespace eq definition pentagon {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z) : whisker_left p (con.assoc' q r s) ⬝ con.assoc' p (q ⬝ r) s - ⬝ whisker_right (con.assoc' p q r) s + ⬝ whisker_right s (con.assoc' p q r) = con.assoc' p q (r ⬝ s) ⬝ con.assoc' (p ⬝ q) r s := by induction s;induction r;induction q;induction p;reflexivity -- The 3-cell witnessing the left unit triangle. definition triangulator (p : x = y) (q : y = z) : - con.assoc' p idp q ⬝ whisker_right (con_idp p) q = whisker_left p (idp_con q) := + con.assoc' p idp q ⬝ whisker_right q (con_idp p) = whisker_left p (idp_con q) := by induction q; induction p; reflexivity definition eckmann_hilton (p q : idp = idp :> a = a) : p ⬝ q = q ⬝ p := diff --git a/hott/types/arrow_2.hlean b/hott/types/arrow_2.hlean index a2f30d600..646a43250 100644 --- a/hott/types/arrow_2.hlean +++ b/hott/types/arrow_2.hlean @@ -158,7 +158,7 @@ namespace arrow (p (f⁻¹ b))⁻¹], apply eq_of_square, refine vconcat_eq _ - (whisker_right (ap_inv β (right_inv f b)) (p (f⁻¹ b))⁻¹)⁻¹, + (whisker_right (p (f⁻¹ b))⁻¹ (ap_inv β (right_inv f b)))⁻¹, refine vconcat_eq _ (con_inv (p (f⁻¹ b)) (ap β (right_inv f b))), refine vconcat_eq _ diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 6cea33033..ad06226a2 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -28,7 +28,7 @@ namespace eq end theorem whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'') - : whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q := + : whisker_right q (r ⬝ s) = whisker_right q r ⬝ whisker_right q s := begin induction q, induction r, induction s, reflexivity end @@ -40,7 +40,7 @@ namespace eq end theorem whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p') - : whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc := + : 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 @@ -56,7 +56,7 @@ namespace eq by induction r; reflexivity theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p') - : whisker_right r⁻¹ q = (whisker_right r q)⁻¹ := + : 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) : @@ -75,7 +75,7 @@ namespace eq by induction p;reflexivity theorem 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_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 @@ -282,7 +282,7 @@ namespace eq equiv.mk _ !is_equiv_whisker_left definition is_equiv_whisker_right [constructor] {p q : a₁ = a₂} (r : a₂ = a₃) - : is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) := + : is_equiv (λs, whisker_right r s : p = q → p ⬝ r = q ⬝ r) := begin fapply adjointify, {intro s, apply (!cancel_right s)}, diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 108368c65..0af87c124 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -164,10 +164,10 @@ namespace is_equiv intro q, apply eq_of_homotopy, intro c, unfold inv_homotopy_of_homotopy_post, unfold homotopy_of_inv_homotopy_post, - apply trans (whisker_right + apply trans (whisker_right (left_inv f (α c)) (ap_con f⁻¹ (right_inv f (β c))⁻¹ (ap f (q c)) - ⬝ whisker_right (ap_inv f⁻¹ (right_inv f (β c))) - (ap f⁻¹ (ap f (q c)))) (left_inv f (α c))), + ⬝ whisker_right (ap f⁻¹ (ap f (q c))) + (ap_inv f⁻¹ (right_inv f (β c))))), apply inverse, apply eq_bot_of_square, apply eq_hconcat (adj_inv f (β c))⁻¹, apply eq_vconcat (ap_compose f⁻¹ f (q c))⁻¹, diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 969245261..c9f2328e0 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -299,11 +299,11 @@ lemma madd_left_inv : Π i : fin (succ n), madd (minv i) i = fin.zero n | (mk iv ilt) := eq_of_veq (by rewrite [val_madd, ↑minv, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self]) -definition madd_is_comm_group [instance] : add_comm_group (fin (succ n)) := -comm_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm +definition madd_is_ab_group [instance] : add_ab_group (fin (succ n)) := +ab_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm -definition gfin (n : ℕ) [H : is_succ n] : AddCommGroup.{0} := -by induction H with n; exact AddCommGroup.mk (fin (succ n)) _ +definition gfin (n : ℕ) [H : is_succ n] : AddAbGroup.{0} := +by induction H with n; exact AddAbGroup.mk (fin (succ n)) _ end madd diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 4bba2fe2b..90d4f691f 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -24,10 +24,10 @@ namespace int notation `gℤ` := group_integers - definition CommGroup_int [reducible] [constructor] : AddCommGroup := - AddCommGroup.mk ℤ _ + definition AbGroup_int [reducible] [constructor] : AddAbGroup := + AddAbGroup.mk ℤ _ - notation `agℤ` := CommGroup_int + notation `agℤ` := AbGroup_int end definition is_equiv_succ [constructor] [instance] : is_equiv succ := diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index dc2781206..73feb5d0e 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -383,7 +383,7 @@ namespace pointed (respect_pt g)) ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), respect_pt f = ap10 p pt ⬝ respect_pt g : sigma_equiv_sigma_right - (λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) + (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _))) ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), respect_pt f = p pt ⬝ respect_pt g : sigma_equiv_sigma_left' eq_equiv_homotopy ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ respect_pt g = respect_pt f @@ -448,7 +448,7 @@ namespace pointed begin fconstructor, { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, - refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, + refine whisker_right _ !ap_inv ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, exact !inv_inv⁻¹}, { induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity}, end diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index ecefc3588..77c0e6d27 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -764,8 +764,8 @@ namespace trunc begin fapply phomotopy.mk, { apply trunc_functor_compose}, - { esimp, refine !idp_con ⬝ _, refine whisker_right !ap_compose'⁻¹ᵖ _ ⬝ _, - esimp, refine whisker_right (ap_compose' tr g _) _ ⬝ _, exact !ap_con⁻¹}, + { esimp, refine !idp_con ⬝ _, refine whisker_right _ !ap_compose'⁻¹ᵖ ⬝ _, + esimp, refine whisker_right _ (ap_compose' tr g _) ⬝ _, exact !ap_con⁻¹}, end definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) : @@ -851,7 +851,7 @@ namespace trunc begin fapply phomotopy.mk, { intro x, induction x with a, reflexivity }, - { esimp, exact !idp_con ⬝ whisker_right !ap_compose _ }, + { esimp, exact !idp_con ⬝ whisker_right _ !ap_compose }, end end trunc open trunc diff --git a/tests/lean/hott/614.hlean b/tests/lean/hott/614.hlean index 075fb966a..0e5d8451b 100644 --- a/tests/lean/hott/614.hlean +++ b/tests/lean/hott/614.hlean @@ -8,7 +8,7 @@ protected definition my_decode {x : circle} (c : circle.code x) : base = x := begin induction x, { revert c, exact power loop }, - { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, + { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r, rewrite [power_con,transport_code_loop]}, end @@ -16,6 +16,6 @@ protected definition my_decode' {x : circle} : circle.code x → base = x := begin induction x, { exact power loop}, - { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, + { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r, rewrite [power_con,transport_code_loop]}, end diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean index 021003ab5..cb39984e1 100644 --- a/tests/lean/hott/615.hlean +++ b/tests/lean/hott/615.hlean @@ -15,6 +15,6 @@ protected definition my_decode {x : circle} : my_code x → base = x := begin induction x, { exact power loop}, - { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, + { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r, xrewrite [power_con, transport_code_loop]}, end diff --git a/tests/lean/hott/beginend2.hlean b/tests/lean/hott/beginend2.hlean index 2a2b9b2a9..c6261c8a5 100644 --- a/tests/lean/hott/beginend2.hlean +++ b/tests/lean/hott/beginend2.hlean @@ -2,7 +2,7 @@ open eq tactic open eq (rec_on) definition concat_whisker2 {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : - (whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') := + (whisker_right q a) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right q' a) := begin apply (rec_on b), apply (rec_on a), diff --git a/tests/lean/hott/rewriter1.hlean b/tests/lean/hott/rewriter1.hlean index bd440b0a9..2bd9ab6d9 100644 --- a/tests/lean/hott/rewriter1.hlean +++ b/tests/lean/hott/rewriter1.hlean @@ -3,7 +3,7 @@ open algebra constant f {A : Type} : A → A → A -theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) := +theorem test1 {A : Type} [s : add_ab_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) := begin rewrite [ add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences @@ -12,7 +12,7 @@ end axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1 -theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 := +theorem test2 {A : Type} [s : ab_group A] (a b c : A) : f a a = 1 := begin rewrite [-(mul_one a), -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences Ax] -- use Ax as rewrite rule diff --git a/tests/lean/hott/rw_binders.hlean b/tests/lean/hott/rw_binders.hlean index 48052ee2a..b0e6c412d 100644 --- a/tests/lean/hott/rw_binders.hlean +++ b/tests/lean/hott/rw_binders.hlean @@ -5,5 +5,5 @@ variables {A : Type} {a1 a2 a3 : A} definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3) : transport (λx, x = a3) p q = p⁻¹ ⬝ q := begin - rewrite transport_eq_l, + rewrite eq_transport_l, end