From 1c52062f1eb40899b0f444f4cf94a4fb3b3f8814 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Mon, 14 Mar 2016 19:11:21 -0400 Subject: [PATCH] chore(hott): standardize names of homotopy_of_inv_homotopy_post and friends --- hott/homotopy/susp.hlean | 9 ++--- hott/init/equiv.hlean | 76 ++++++++++++++++++++++------------------ hott/types/arrow_2.hlean | 22 ++++++------ hott/types/equiv.hlean | 34 +++++++++--------- 4 files changed, 74 insertions(+), 67 deletions(-) diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 7593a460a..aab3ab608 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -225,11 +225,12 @@ namespace susp begin fconstructor, { intro a, induction a, - { reflexivity}, - { reflexivity}, + { reflexivity }, + { reflexivity }, { apply eq_pathover, apply hdeg_square, - rewrite [▸*,ap_compose' _ (psusp_functor f),↑psusp_functor,+elim_merid]}}, - { reflexivity} + rewrite [▸*,ap_compose' _ (psusp_functor f),↑psusp_functor], + krewrite +susp.elim_merid } }, + { reflexivity } end -- adjunction from Coq-HoTT diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 697335c92..cd5174045 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -198,34 +198,57 @@ namespace is_equiv end section - variables {A B C : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B} {g : B → C} {h : A → C} + variables {A B C : Type} {f : A → B} [Hf : is_equiv f] include Hf - --Rewrite rules - definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := - ap f p ⬝ right_inv f b + section rewrite_rules + variables {a : A} {b : B} + definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b := + ap f p ⬝ right_inv f b - definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := - (eq_of_eq_inv p⁻¹)⁻¹ + definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a := + (eq_of_eq_inv p⁻¹)⁻¹ - definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := - ap f⁻¹ p ⬝ left_inv f a + definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a := + ap f⁻¹ p ⬝ left_inv f a - definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := - (inv_eq_of_eq p⁻¹)⁻¹ + definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b := + (inv_eq_of_eq p⁻¹)⁻¹ + end rewrite_rules variable (f) - definition homotopy_of_homotopy_inv' (p : g ~ h ∘ f⁻¹) : g ∘ f ~ h := - λa, p (f a) ⬝ ap h (left_inv f a) - definition homotopy_of_inv_homotopy' (p : h ∘ f⁻¹ ~ g) : h ~ g ∘ f := - λa, ap h (left_inv f a)⁻¹ ⬝ p (f a) + section pre_compose + variables (α : A → C) (β : B → C) - definition inv_homotopy_of_homotopy' (p : h ~ g ∘ f) : h ∘ f⁻¹ ~ g := - λb, p (f⁻¹ b) ⬝ ap g (right_inv f b) + definition homotopy_of_homotopy_inv_pre (p : β ~ α ∘ f⁻¹) : β ∘ f ~ α := + λ a, p (f a) ⬝ ap α (left_inv f a) - definition homotopy_inv_of_homotopy' (p : g ∘ f ~ h) : g ~ h ∘ f⁻¹ := - λb, ap g (right_inv f b)⁻¹ ⬝ p (f⁻¹ b) + definition homotopy_of_inv_homotopy_pre (p : α ∘ f⁻¹ ~ β) : α ~ β ∘ f := + λ a, (ap α (left_inv f a))⁻¹ ⬝ p (f a) + + definition inv_homotopy_of_homotopy_pre (p : α ~ β ∘ f) : α ∘ f⁻¹ ~ β := + λ b, p (f⁻¹ b) ⬝ ap β (right_inv f b) + + definition homotopy_inv_of_homotopy_pre (p : β ∘ f ~ α) : β ~ α ∘ f⁻¹ := + λ b, (ap β (right_inv f b))⁻¹ ⬝ p (f⁻¹ b) + end pre_compose + + section post_compose + variables (α : C → A) (β : C → B) + + definition homotopy_of_homotopy_inv_post (p : α ~ f⁻¹ ∘ β) : f ∘ α ~ β := + λ c, ap f (p c) ⬝ (right_inv f (β c)) + + definition homotopy_of_inv_homotopy_post (p : f⁻¹ ∘ β ~ α) : β ~ f ∘ α := + λ c, (right_inv f (β c))⁻¹ ⬝ ap f (p c) + + definition inv_homotopy_of_homotopy_post (p : β ~ f ∘ α) : f⁻¹ ∘ β ~ α := + λ c, ap f⁻¹ (p c) ⬝ (left_inv f (α c)) + + definition homotopy_inv_of_homotopy_post (p : f ∘ α ~ β) : α ~ f⁻¹ ∘ β := + λ c, (left_inv f (α c))⁻¹ ⬝ ap f⁻¹ (p c) + end post_compose end @@ -374,23 +397,6 @@ namespace equiv end - section - variables {A B C : Type} (f : A ≃ B) {a : A} {b : B} {g : B → C} {h : A → C} - - definition homotopy_of_homotopy_inv (p : g ~ h ∘ f⁻¹) : g ∘ f ~ h := - homotopy_of_homotopy_inv' f p - - definition homotopy_of_inv_homotopy (p : h ∘ f⁻¹ ~ g) : h ~ g ∘ f := - homotopy_of_inv_homotopy' f p - - definition inv_homotopy_of_homotopy (p : h ~ g ∘ f) : h ∘ f⁻¹ ~ g := - inv_homotopy_of_homotopy' f p - - definition homotopy_inv_of_homotopy (p : g ∘ f ~ h) : g ~ h ∘ f⁻¹ := - homotopy_inv_of_homotopy' f p - - end - infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq infixl ` ⬝ep `:75 := equiv_of_eq_of_equiv diff --git a/hott/types/arrow_2.hlean b/hott/types/arrow_2.hlean index fa6837006..e398f6fcc 100644 --- a/hott/types/arrow_2.hlean +++ b/hott/types/arrow_2.hlean @@ -124,9 +124,9 @@ namespace arrow open function definition inv_commute_of_commute (p : f' ∘ α ~ β ∘ f) : f'⁻¹ ∘ β ~ α ∘ f⁻¹ := begin - apply homotopy_inv_of_homotopy_post f' β (α ∘ f⁻¹), + apply inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹) β, apply homotopy.symm, - apply homotopy_inv_of_homotopy_pre f (f' ∘ α) β, + apply inv_homotopy_of_homotopy_pre f (f' ∘ α) β, apply p end @@ -135,8 +135,8 @@ namespace arrow = (ap f'⁻¹ (p a))⁻¹ ⬝ left_inv f' (α a) ⬝ ap α (left_inv f a)⁻¹ := begin unfold inv_commute_of_commute, - unfold homotopy_inv_of_homotopy_post, - unfold homotopy_inv_of_homotopy_pre, + unfold inv_homotopy_of_homotopy_post, + unfold inv_homotopy_of_homotopy_pre, rewrite [adj f a,-(ap_compose β f)], rewrite [eq_of_square (natural_square_tr p (left_inv f a))], rewrite [ap_inv f'⁻¹,ap_con f'⁻¹,con_inv,con.assoc,con.assoc], @@ -152,8 +152,8 @@ namespace arrow = right_inv f' (β b) ⬝ ap β (right_inv f b)⁻¹ ⬝ (p (f⁻¹ b))⁻¹ := begin unfold inv_commute_of_commute, - unfold homotopy_inv_of_homotopy_post, - unfold homotopy_inv_of_homotopy_pre, + unfold inv_homotopy_of_homotopy_post, + unfold inv_homotopy_of_homotopy_pre, rewrite [ap_con,-(ap_compose f' f'⁻¹),-(adj f' (α (f⁻¹ b)))], rewrite [con.assoc (right_inv f' (β b)) (ap β (right_inv f b)⁻¹) (p (f⁻¹ b))⁻¹], @@ -173,13 +173,13 @@ namespace arrow begin unfold inv_commute_of_commute, apply @is_equiv_compose _ _ _ - (homotopy.symm ∘ (homotopy_inv_of_homotopy_pre f (f' ∘ α) β)) - (homotopy_inv_of_homotopy_post f' β (α ∘ f⁻¹)), + (homotopy.symm ∘ (inv_homotopy_of_homotopy_pre f (f' ∘ α) β)) + (inv_homotopy_of_homotopy_post f' (α ∘ f⁻¹) β), { apply @is_equiv_compose _ _ _ - (homotopy_inv_of_homotopy_pre f (f' ∘ α) β) homotopy.symm, - { apply homotopy_inv_of_homotopy_pre.is_equiv }, + (inv_homotopy_of_homotopy_pre f (f' ∘ α) β) homotopy.symm, + { apply inv_homotopy_of_homotopy_pre.is_equiv }, { apply pi.is_equiv_homotopy_symm } }, - { apply homotopy_inv_of_homotopy_post.is_equiv } + { apply inv_homotopy_of_homotopy_post.is_equiv } end end arrow diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index b8ae60a34..354deef33 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -111,15 +111,14 @@ namespace is_equiv section pre_compose variables (α : A → C) (β : B → C) - definition homotopy_inv_of_homotopy_pre (p : α ~ β ∘ f) : α ∘ f⁻¹ ~ β := - λb, p (f⁻¹ b) ⬝ ap β (right_inv f b) - - protected definition homotopy_inv_of_homotopy_pre.is_equiv - : is_equiv (homotopy_inv_of_homotopy_pre f α β) := - adjointify _ (λq a, (ap α (left_inv f a))⁻¹ ⬝ q (f a)) + -- homotopy_inv_of_homotopy_pre is in init.equiv + protected definition inv_homotopy_of_homotopy_pre.is_equiv + : is_equiv (inv_homotopy_of_homotopy_pre f α β) := + adjointify _ (homotopy_of_inv_homotopy_pre f α β) abstract begin intro q, apply eq_of_homotopy, intro b, - unfold homotopy_inv_of_homotopy_pre, + unfold inv_homotopy_of_homotopy_pre, + unfold homotopy_of_inv_homotopy_pre, apply inverse, apply eq_bot_of_square, apply eq_hconcat (ap02 α (adj_inv f b)), apply eq_hconcat (ap_compose α f⁻¹ (right_inv f b))⁻¹, @@ -127,7 +126,8 @@ namespace is_equiv end end abstract begin intro p, apply eq_of_homotopy, intro a, - unfold homotopy_inv_of_homotopy_pre, + unfold inv_homotopy_of_homotopy_pre, + unfold homotopy_of_inv_homotopy_pre, apply trans (con.assoc (ap α (left_inv f a))⁻¹ (p (f⁻¹ (f a))) @@ -140,17 +140,16 @@ namespace is_equiv end pre_compose section post_compose - variables (β : C → B) (α : C → A) + variables (α : C → A) (β : C → B) - definition homotopy_inv_of_homotopy_post (p : β ~ f ∘ α) : f⁻¹ ∘ β ~ α := - λc, ap f⁻¹ (p c) ⬝ (left_inv f (α c)) - - protected definition homotopy_inv_of_homotopy_post.is_equiv - : is_equiv (homotopy_inv_of_homotopy_post f β α) := - adjointify _ (λq c, (right_inv f (β c))⁻¹ ⬝ ap f (q c)) + -- homotopy_inv_of_homotopy_post is in init.equiv + protected definition inv_homotopy_of_homotopy_post.is_equiv + : is_equiv (inv_homotopy_of_homotopy_post f α β) := + adjointify _ (homotopy_of_inv_homotopy_post f α β) abstract begin intro q, apply eq_of_homotopy, intro c, - unfold homotopy_inv_of_homotopy_post, + unfold inv_homotopy_of_homotopy_post, + unfold homotopy_of_inv_homotopy_post, apply trans (whisker_right (ap_con f⁻¹ (right_inv f (β c))⁻¹ (ap f (q c)) ⬝ whisker_right (ap_inv f⁻¹ (right_inv f (β c))) @@ -163,7 +162,8 @@ namespace is_equiv end end abstract begin intro p, apply eq_of_homotopy, intro c, - unfold homotopy_inv_of_homotopy_post, + unfold inv_homotopy_of_homotopy_post, + unfold homotopy_of_inv_homotopy_post, apply trans (whisker_left (right_inv f (β c))⁻¹ (ap_con f (ap f⁻¹ (p c)) (left_inv f (α c)))), apply trans (con.assoc (right_inv f (β c))⁻¹ (ap f (ap f⁻¹ (p c)))