From b94b66243e9599bfcbc4bb8d8076eb9a6ed01134 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 23 Jun 2015 13:21:04 -0400 Subject: [PATCH] feat(hott/types): add some theorems about operations of 2-paths --- hott/types/cubical/square.hlean | 19 +++- hott/types/eq.hlean | 177 ++++++++++++++++++-------------- hott/types/eq2.hlean | 108 +++++++++++++++++++ 3 files changed, 227 insertions(+), 77 deletions(-) create mode 100644 hott/types/eq2.hlean diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean index 357a95f5da..45e8284d01 100644 --- a/hott/types/cubical/square.hlean +++ b/hott/types/cubical/square.hlean @@ -10,7 +10,7 @@ open eq equiv is_equiv namespace eq - variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} + variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ @@ -157,6 +157,9 @@ namespace eq definition eq_of_vdeg_square [reducible] {p q : a = a'} (s : square p q idp idp) : p = q := to_fun !vdeg_square_equiv' s + definition top_deg_square (l : a₁ = a₂) (b : a₂ = a₃) (r : a₄ = a₃) : square (l ⬝ b ⬝ r⁻¹) b l r := + by induction r;induction b;induction l;constructor + /- the following two equivalences have as underlying inverse function the functions hdeg_square and vdeg_square, respectively. @@ -342,4 +345,18 @@ namespace eq --we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed + /- squares commute with some operations on 2-paths -/ + + definition square_inv2 {p₁ p₂ p₃ p₄ : a = a'} + {t : p₁ = p₂} {b : p₃ = p₄} {l : p₁ = p₃} {r : p₂ = p₄} (s : square t b l r) + : square (inverse2 t) (inverse2 b) (inverse2 l) (inverse2 r) := + by induction s;constructor + + definition square_con2 {p₁ p₂ p₃ p₄ : a₁ = a₂} {q₁ q₂ q₃ q₄ : a₂ = a₃} + {t₁ : p₁ = p₂} {b₁ : p₃ = p₄} {l₁ : p₁ = p₃} {r₁ : p₂ = p₄} + {t₂ : q₁ = q₂} {b₂ : q₃ = q₄} {l₂ : q₁ = q₃} {r₂ : q₂ = q₄} + (s₁ : square t₁ b₁ l₁ r₁) (s₂ : square t₂ b₂ l₂ r₂) + : square (t₁ ◾ t₂) (b₁ ◾ b₂) (l₁ ◾ l₂) (r₁ ◾ r₂) := + by induction s₂;induction s₁;constructor + end eq diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 53e1c8b1c8..ebac2f48f2 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -14,49 +14,49 @@ open eq sigma sigma.ops equiv is_equiv equiv.ops namespace eq /- Path spaces -/ - variables {A B : Type} {a a1 a2 a3 a4 : A} {b b1 b2 : B} {f g : A → B} {h : B → A} - {p p' p'' : a1 = a2} + variables {A B : Type} {a a₁ a₂ a₃ a₄ a' : A} {b b1 b2 : B} {f g : A → B} {h : B → A} + {p p' p'' : a₁ = a₂} /- The path spaces of a path space are not, of course, determined; they are just the higher-dimensional structure of the original space. -/ /- some lemmas about whiskering or other higher paths -/ - theorem whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'') + theorem 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 : a2 = a3) (r : p = p') (s : p' = p'') + 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 := begin induction q, induction r, induction s, reflexivity end - theorem whisker_left_con_left (p : a1 = a2) (p' : a2 = a3) {q q' : a3 = a4} (r : q = q') + theorem 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' : a1 = a2} (q : a2 = a3) (q' : a3 = a4) (r : p = p') + 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 := begin induction q', induction q, induction r, induction p, reflexivity end - theorem whisker_left_inv_left (p : a2 = a1) {q q' : a2 = a3} (r : q = q') + theorem 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 : a1 = a2) {q q' : a2 = a3} (r : q = q') + theorem 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' : a1 = a2} (q : a2 = a3) (r : p = p') + theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p') : whisker_right r⁻¹ q = (whisker_right r q)⁻¹ := by induction r; reflexivity @@ -69,27 +69,52 @@ namespace eq theorem 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 : a1 = a2) + theorem 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 : a1 = a2) + 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 (ap f) (con.left_inv p) := by induction p;reflexivity - theorem idp_con_whisker_left {q q' : a2 = a3} (r : q = q') : + theorem 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' : a2 = a3} (r : q = q') : + theorem 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 := by cases q;reflexivity + definition ap_weakly_constant [unfold-c 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b) + {x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ := + by induction q;exact !con.right_inv⁻¹ + + definition inv2_inv {p q : a = a'} (r : p = q) : inverse2 r⁻¹ = (inverse2 r)⁻¹ := + by induction r;reflexivity + + definition inv2_con {p p' p'' : a = a'} (r : p = p') (r' : p' = p'') + : inverse2 (r ⬝ r') = inverse2 r ⬝ inverse2 r' := + by induction r';induction r;reflexivity + + definition con2_inv {p₁ q₁ : a₁ = a₂} {p₂ q₂ : a₂ = a₃} (r₁ : p₁ = q₁) (r₂ : p₂ = q₂) + : (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} + {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) : + con.right_inv p = r ◾ inverse2 r := + by cases r;reflexivity + /- Transporting in path spaces. There are potentially a lot of these lemmas, so we adopt a uniform naming scheme: @@ -99,40 +124,40 @@ namespace eq - `F` means application of a function to that (varying) endpoint. -/ - definition transport_eq_l (p : a1 = a2) (q : a1 = a3) - : transport (λx, x = a3) p q = p⁻¹ ⬝ q := + definition transport_eq_l (p : a₁ = a₂) (q : a₁ = a₃) + : transport (λx, x = a₃) p q = p⁻¹ ⬝ q := by induction p; induction q; reflexivity - definition transport_eq_r (p : a2 = a3) (q : a1 = a2) - : transport (λx, a1 = x) p q = q ⬝ p := + definition transport_eq_r (p : a₂ = a₃) (q : a₁ = a₂) + : transport (λx, a₁ = x) p q = q ⬝ p := by induction p; induction q; reflexivity - definition transport_eq_lr (p : a1 = a2) (q : a1 = a1) + definition transport_eq_lr (p : a₁ = a₂) (q : a₁ = a₁) : transport (λx, x = x) p q = p⁻¹ ⬝ q ⬝ p := by induction p; rewrite [▸*,idp_con] - definition transport_eq_Fl (p : a1 = a2) (q : f a1 = b) + definition transport_eq_Fl (p : a₁ = a₂) (q : f a₁ = b) : transport (λx, f x = b) p q = (ap f p)⁻¹ ⬝ q := by induction p; induction q; reflexivity - definition transport_eq_Fr (p : a1 = a2) (q : b = f a1) + definition transport_eq_Fr (p : a₁ = a₂) (q : b = f a₁) : transport (λx, b = f x) p q = q ⬝ (ap f p) := by induction p; reflexivity - definition transport_eq_FlFr (p : a1 = a2) (q : f a1 = g a1) + definition transport_eq_FlFr (p : a₁ = a₂) (q : f a₁ = g a₁) : transport (λx, f x = g x) p q = (ap f p)⁻¹ ⬝ q ⬝ (ap g p) := by induction p; rewrite [▸*,idp_con] definition transport_eq_FlFr_D {B : A → Type} {f g : Πa, B a} - (p : a1 = a2) (q : f a1 = g a1) + (p : a₁ = a₂) (q : f a₁ = g a₁) : transport (λx, f x = g x) p q = (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := by induction p; rewrite [▸*,idp_con,ap_id] - definition transport_eq_FFlr (p : a1 = a2) (q : h (f a1) = a1) + definition transport_eq_FFlr (p : a₁ = a₂) (q : h (f a₁) = a₁) : transport (λx, h (f x) = x) p q = (ap h (ap f p))⁻¹ ⬝ q ⬝ p := by induction p; rewrite [▸*,idp_con] - definition transport_eq_lFFr (p : a1 = a2) (q : a1 = h (f a1)) + definition transport_eq_lFFr (p : a₁ = a₂) (q : a₁ = h (f a₁)) : transport (λx, x = h (f x)) p q = p⁻¹ ⬝ q ⬝ (ap h (ap f p)) := by induction p; rewrite [▸*,idp_con] @@ -143,44 +168,44 @@ namespace eq -- we should probably try to do everything just with pathover_eq (defined in cubical.square), -- the following definitions may be removed in future. - definition pathover_eq_l (p : a1 = a2) (q : a1 = a3) : q =[p] p⁻¹ ⬝ q := /-(λx, x = a3)-/ + definition pathover_eq_l (p : a₁ = a₂) (q : a₁ = a₃) : q =[p] p⁻¹ ⬝ q := /-(λx, x = a₃)-/ by induction p; induction q; exact idpo - definition pathover_eq_r (p : a2 = a3) (q : a1 = a2) : q =[p] q ⬝ p := /-(λx, a1 = x)-/ + definition pathover_eq_r (p : a₂ = a₃) (q : a₁ = a₂) : q =[p] q ⬝ p := /-(λx, a₁ = x)-/ by induction p; induction q; exact idpo - definition pathover_eq_lr (p : a1 = a2) (q : a1 = a1) : q =[p] p⁻¹ ⬝ q ⬝ p := /-(λx, x = x)-/ + definition pathover_eq_lr (p : a₁ = a₂) (q : a₁ = a₁) : q =[p] p⁻¹ ⬝ q ⬝ p := /-(λx, x = x)-/ by induction p; rewrite [▸*,idp_con]; exact idpo - definition pathover_eq_Fl (p : a1 = a2) (q : f a1 = b) : q =[p] (ap f p)⁻¹ ⬝ q := /-(λx, f x = b)-/ + definition pathover_eq_Fl (p : a₁ = a₂) (q : f a₁ = b) : q =[p] (ap f p)⁻¹ ⬝ q := /-(λx, f x = b)-/ by induction p; induction q; exact idpo - definition pathover_eq_Fr (p : a1 = a2) (q : b = f a1) : q =[p] q ⬝ (ap f p) := /-(λx, b = f x)-/ + definition pathover_eq_Fr (p : a₁ = a₂) (q : b = f a₁) : q =[p] q ⬝ (ap f p) := /-(λx, b = f x)-/ by induction p; exact idpo - definition pathover_eq_FlFr (p : a1 = a2) (q : f a1 = g a1) : q =[p] (ap f p)⁻¹ ⬝ q ⬝ (ap g p) := + definition pathover_eq_FlFr (p : a₁ = a₂) (q : f a₁ = g a₁) : q =[p] (ap f p)⁻¹ ⬝ q ⬝ (ap g p) := /-(λx, f x = g x)-/ by induction p; rewrite [▸*,idp_con]; exact idpo - definition pathover_eq_FlFr_D {B : A → Type} {f g : Πa, B a} (p : a1 = a2) (q : f a1 = g a1) + definition pathover_eq_FlFr_D {B : A → Type} {f g : Πa, B a} (p : a₁ = a₂) (q : f a₁ = g a₁) : q =[p] (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := /-(λx, f x = g x)-/ by induction p; rewrite [▸*,idp_con,ap_id];exact idpo - definition pathover_eq_FFlr (p : a1 = a2) (q : h (f a1) = a1) : q =[p] (ap h (ap f p))⁻¹ ⬝ q ⬝ p := + definition pathover_eq_FFlr (p : a₁ = a₂) (q : h (f a₁) = a₁) : q =[p] (ap h (ap f p))⁻¹ ⬝ q ⬝ p := /-(λx, h (f x) = x)-/ by induction p; rewrite [▸*,idp_con];exact idpo - definition pathover_eq_lFFr (p : a1 = a2) (q : a1 = h (f a1)) : q =[p] p⁻¹ ⬝ q ⬝ (ap h (ap f p)) := + definition pathover_eq_lFFr (p : a₁ = a₂) (q : a₁ = h (f a₁)) : q =[p] p⁻¹ ⬝ q ⬝ (ap h (ap f p)) := /-(λx, x = h (f x))-/ by induction p; rewrite [▸*,idp_con];exact idpo - definition pathover_eq_r_idp (p : a1 = a2) : idp =[p] p := /-(λx, a1 = x)-/ + definition pathover_eq_r_idp (p : a₁ = a₂) : idp =[p] p := /-(λx, a₁ = x)-/ by induction p; exact idpo - definition pathover_eq_l_idp (p : a1 = a2) : idp =[p] p⁻¹ := /-(λx, x = a1)-/ + definition pathover_eq_l_idp (p : a₁ = a₂) : idp =[p] p⁻¹ := /-(λx, x = a₁)-/ by induction p; exact idpo - definition pathover_eq_l_idp' (p : a1 = a2) : idp =[p⁻¹] p := /-(λx, x = a2)-/ + definition pathover_eq_l_idp' (p : a₁ = a₂) : idp =[p⁻¹] p := /-(λx, x = a₂)-/ by induction p; exact idpo -- The Functorial action of paths is [ap]. @@ -189,46 +214,46 @@ namespace eq /- [ap_closed] is in init.equiv -/ - definition equiv_ap (f : A → B) [H : is_equiv f] (a1 a2 : A) - : (a1 = a2) ≃ (f a1 = f a2) := + definition equiv_ap (f : A → B) [H : is_equiv f] (a₁ a₂ : A) + : (a₁ = a₂) ≃ (f a₁ = f a₂) := equiv.mk (ap f) _ /- Path operations are equivalences -/ - definition is_equiv_eq_inverse (a1 a2 : A) : is_equiv (@inverse A a1 a2) := + definition is_equiv_eq_inverse (a₁ a₂ : A) : is_equiv (@inverse A a₁ a₂) := 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) := + definition eq_equiv_eq_symm (a₁ a₂ : A) : (a₁ = a₂) ≃ (a₂ = a₁) := equiv.mk inverse _ - definition is_equiv_concat_left [constructor] [instance] (p : a1 = a2) (a3 : A) - : is_equiv (concat p : a2 = a3 → a1 = a3) := + definition is_equiv_concat_left [constructor] [instance] (p : a₁ = a₂) (a₃ : A) + : is_equiv (concat p : a₂ = a₃ → a₁ = a₃) := is_equiv.mk (concat p) (concat p⁻¹) (con_inv_cancel_left p) (inv_con_cancel_left p) (λq, by induction p;induction q;reflexivity) local attribute is_equiv_concat_left [instance] - definition equiv_eq_closed_left [constructor] (a3 : A) (p : a1 = a2) : (a1 = a3) ≃ (a2 = a3) := + definition equiv_eq_closed_left [constructor] (a₃ : A) (p : a₁ = a₂) : (a₁ = a₃) ≃ (a₂ = a₃) := equiv.mk (concat p⁻¹) _ - definition is_equiv_concat_right [constructor] [instance] (p : a2 = a3) (a1 : A) - : is_equiv (λq : a1 = a2, q ⬝ p) := + definition is_equiv_concat_right [constructor] [instance] (p : a₂ = a₃) (a₁ : A) + : is_equiv (λq : a₁ = a₂, 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) (λq, by induction p;induction q;reflexivity) local attribute is_equiv_concat_right [instance] - definition equiv_eq_closed_right [constructor] (a1 : A) (p : a2 = a3) : (a1 = a2) ≃ (a1 = a3) := + definition equiv_eq_closed_right [constructor] (a₁ : A) (p : a₂ = a₃) : (a₁ = a₂) ≃ (a₁ = a₃) := equiv.mk (λq, q ⬝ p) _ - definition eq_equiv_eq_closed [constructor] (p : a1 = a2) (q : a3 = a4) : (a1 = a3) ≃ (a2 = a4) := - equiv.trans (equiv_eq_closed_left a3 p) (equiv_eq_closed_right a2 q) + definition eq_equiv_eq_closed [constructor] (p : a₁ = a₂) (q : a₃ = a₄) : (a₁ = a₃) ≃ (a₂ = a₄) := + equiv.trans (equiv_eq_closed_left a₃ p) (equiv_eq_closed_right a₂ q) - definition is_equiv_whisker_left (p : a1 = a2) (q r : a2 = a3) - : is_equiv (@whisker_left A a1 a2 a3 p q r) := + definition is_equiv_whisker_left (p : a₁ = a₂) (q r : a₂ = a₃) + : is_equiv (@whisker_left A a₁ a₂ a₃ p q r) := begin fapply adjointify, {intro s, apply (!cancel_left s)}, @@ -244,11 +269,11 @@ namespace eq {intro s, induction s, induction q, induction p, reflexivity} end - definition eq_equiv_con_eq_con_left (p : a1 = a2) (q r : a2 = a3) : (q = r) ≃ (p ⬝ q = p ⬝ r) := + definition eq_equiv_con_eq_con_left (p : a₁ = a₂) (q r : a₂ = a₃) : (q = r) ≃ (p ⬝ q = p ⬝ r) := equiv.mk _ !is_equiv_whisker_left - definition is_equiv_whisker_right {p q : a1 = a2} (r : a2 = a3) - : is_equiv (λs, @whisker_right A a1 a2 a3 p q s r) := + definition is_equiv_whisker_right {p q : a₁ = a₂} (r : a₂ = a₃) + : is_equiv (λs, @whisker_right A a₁ a₂ a₃ p q s r) := begin fapply adjointify, {intro s, apply (!cancel_right s)}, @@ -256,7 +281,7 @@ namespace eq {intro s, induction s, induction r, induction p, reflexivity} end - definition eq_equiv_con_eq_con_right (p q : a1 = a2) (r : a2 = a3) : (p = q) ≃ (p ⬝ r = q ⬝ r) := + definition eq_equiv_con_eq_con_right (p q : a₁ = a₂) (r : a₂ = a₃) : (p = q) ≃ (p ⬝ r = q ⬝ r) := equiv.mk _ !is_equiv_whisker_right /- @@ -264,7 +289,7 @@ namespace eq However, these proofs have the advantage that the inverse is definitionally equal to what we would expect -/ - definition is_equiv_con_eq_of_eq_inv_con (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_con_eq_of_eq_inv_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_eq_of_eq_inv_con : p = r⁻¹ ⬝ q → r ⬝ p = q) := begin fapply adjointify, @@ -275,11 +300,11 @@ namespace eq con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end - definition eq_inv_con_equiv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition eq_inv_con_equiv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : (p = r⁻¹ ⬝ q) ≃ (r ⬝ p = q) := equiv.mk _ !is_equiv_con_eq_of_eq_inv_con - definition is_equiv_con_eq_of_eq_con_inv (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_con_eq_of_eq_con_inv (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_eq_of_eq_con_inv : r = q ⬝ p⁻¹ → r ⬝ p = q) := begin fapply adjointify, @@ -288,11 +313,11 @@ namespace eq { intro s, induction p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq]] }, end - definition eq_con_inv_equiv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition eq_con_inv_equiv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : (r = q ⬝ p⁻¹) ≃ (r ⬝ p = q) := equiv.mk _ !is_equiv_con_eq_of_eq_con_inv - definition is_equiv_inv_con_eq_of_eq_con (p : a1 = a3) (q : a2 = a3) (r : a1 = a2) + definition is_equiv_inv_con_eq_of_eq_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) : is_equiv (inv_con_eq_of_eq_con : p = r ⬝ q → r⁻¹ ⬝ p = q) := begin fapply adjointify, @@ -303,11 +328,11 @@ namespace eq con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end - definition eq_con_equiv_inv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a1 = a2) + definition eq_con_equiv_inv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) : (p = r ⬝ q) ≃ (r⁻¹ ⬝ p = q) := equiv.mk _ !is_equiv_inv_con_eq_of_eq_con - definition is_equiv_con_inv_eq_of_eq_con (p : a3 = a1) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_con_inv_eq_of_eq_con (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_inv_eq_of_eq_con : r = q ⬝ p → r ⬝ p⁻¹ = q) := begin fapply adjointify, @@ -316,7 +341,7 @@ namespace eq { intro s, induction p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_eq]] }, end - definition eq_con_equiv_con_inv_eq (p : a3 = a1) (q : a2 = a3) (r : a2 = a1) + definition eq_con_equiv_con_inv_eq (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁) : (r = q ⬝ p) ≃ (r ⬝ p⁻¹ = q) := equiv.mk _ !is_equiv_con_inv_eq_of_eq_con @@ -325,54 +350,54 @@ namespace eq is_equiv_con_eq_of_eq_con_inv is_equiv_con_eq_of_eq_inv_con [instance] - definition is_equiv_eq_con_of_inv_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_eq_con_of_inv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (eq_con_of_inv_con_eq : r⁻¹ ⬝ q = p → q = r ⬝ p) := is_equiv_inv inv_con_eq_of_eq_con - definition is_equiv_eq_con_of_con_inv_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_eq_con_of_con_inv_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (eq_con_of_con_inv_eq : q ⬝ p⁻¹ = r → q = r ⬝ p) := is_equiv_inv con_inv_eq_of_eq_con - definition is_equiv_eq_con_inv_of_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_eq_con_inv_of_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (eq_con_inv_of_con_eq : r ⬝ p = q → r = q ⬝ p⁻¹) := is_equiv_inv con_eq_of_eq_con_inv - definition is_equiv_eq_inv_con_of_con_eq (p : a1 = a3) (q : a2 = a3) (r : a2 = a1) + definition is_equiv_eq_inv_con_of_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (eq_inv_con_of_con_eq : r ⬝ p = q → p = r⁻¹ ⬝ q) := is_equiv_inv con_eq_of_eq_inv_con /- Pathover Equivalences -/ - definition pathover_eq_equiv_l (p : a1 = a2) (q : a1 = a3) (r : a2 = a3) : q =[p] r ≃ q = p ⬝ r := - /-(λx, x = a3)-/ + definition pathover_eq_equiv_l (p : a₁ = a₂) (q : a₁ = a₃) (r : a₂ = a₃) : q =[p] r ≃ q = p ⬝ r := + /-(λx, x = a₃)-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ - definition pathover_eq_equiv_r (p : a2 = a3) (q : a1 = a2) (r : a1 = a3) : q =[p] r ≃ q ⬝ p = r := - /-(λx, a1 = x)-/ + definition pathover_eq_equiv_r (p : a₂ = a₃) (q : a₁ = a₂) (r : a₁ = a₃) : q =[p] r ≃ q ⬝ p = r := + /-(λx, a₁ = x)-/ by induction p; apply pathover_idp - definition pathover_eq_equiv_lr (p : a1 = a2) (q : a1 = a1) (r : a2 = a2) + definition pathover_eq_equiv_lr (p : a₁ = a₂) (q : a₁ = a₁) (r : a₂ = a₂) : q =[p] r ≃ q ⬝ p = p ⬝ r := /-(λx, x = x)-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ - definition pathover_eq_equiv_Fl (p : a1 = a2) (q : f a1 = b) (r : f a2 = b) + definition pathover_eq_equiv_Fl (p : a₁ = a₂) (q : f a₁ = b) (r : f a₂ = b) : q =[p] r ≃ q = ap f p ⬝ r := /-(λx, f x = b)-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ - definition pathover_eq_equiv_Fr (p : a1 = a2) (q : b = f a1) (r : b = f a2) + definition pathover_eq_equiv_Fr (p : a₁ = a₂) (q : b = f a₁) (r : b = f a₂) : q =[p] r ≃ q ⬝ ap f p = r := /-(λx, b = f x)-/ by induction p; apply pathover_idp - definition pathover_eq_equiv_FlFr (p : a1 = a2) (q : f a1 = g a1) (r : f a2 = g a2) + definition pathover_eq_equiv_FlFr (p : a₁ = a₂) (q : f a₁ = g a₁) (r : f a₂ = g a₂) : q =[p] r ≃ q ⬝ ap g p = ap f p ⬝ r := /-(λx, f x = g x)-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ - definition pathover_eq_equiv_FFlr (p : a1 = a2) (q : h (f a1) = a1) (r : h (f a2) = a2) + definition pathover_eq_equiv_FFlr (p : a₁ = a₂) (q : h (f a₁) = a₁) (r : h (f a₂) = a₂) : q =[p] r ≃ q ⬝ p = ap h (ap f p) ⬝ r := /-(λx, h (f x) = x)-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ - definition pathover_eq_equiv_lFFr (p : a1 = a2) (q : a1 = h (f a1)) (r : a2 = h (f a2)) + definition pathover_eq_equiv_lFFr (p : a₁ = a₂) (q : a₁ = h (f a₁)) (r : a₂ = h (f a₂)) : q =[p] r ≃ q ⬝ ap h (ap f p) = p ⬝ r := /-(λx, x = h (f x))-/ by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ diff --git a/hott/types/eq2.hlean b/hott/types/eq2.hlean new file mode 100644 index 0000000000..1b6b628e22 --- /dev/null +++ b/hott/types/eq2.hlean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Floris van Doorn + +Theorems about 2-dimensional paths +-/ + +import .cubical.square +open function + +namespace eq + variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B} + + theorem ap_weakly_constant_eq (p : Πx, f x = b) (q : a = a') : + ap_weakly_constant p q = + eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apdo p q)))⁻¹ ⬝ + whisker_left (p a) (ap_constant q b)) := + begin + induction q, esimp, generalize (p a), intro p, cases p, apply idpath idp + end + + definition ap_inv2 {p q : a = a'} (r : p = q) + : square (ap (ap f) (inverse2 r)) + (inverse2 (ap (ap f) r)) + (ap_inv f p) + (ap_inv f q) := + by induction r;exact hrfl + + definition ap_con2 {p₁ q₁ : a₁ = a₂} {p₂ q₂ : a₂ = a₃} (r₁ : p₁ = q₁) (r₂ : p₂ = q₂) + : square (ap (ap f) (r₁ ◾ r₂)) + (ap (ap f) r₁ ◾ ap (ap f) r₂) + (ap_con f p₁ p₂) + (ap_con f q₁ q₂) := + by induction r₂;induction r₁;exact hrfl + + theorem ap_con_right_inv_sq {A B : Type} {a1 a2 : A} (f : A → B) (p : a1 = a2) : + square (ap (ap f) (con.right_inv p)) + (con.right_inv (ap f p)) + (ap_con f p p⁻¹ ⬝ whisker_left _ (ap_inv f p)) + idp := + by cases p;apply hrefl + + 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) _) + idp := + by cases p;apply vrefl + + theorem ap_ap_weakly_constant {A B C : Type} (g : B → C) {f : A → B} {b : B} + (p : Πx, f x = b) {x y : A} (q : x = y) : + square (ap (ap g) (ap_weakly_constant p q)) + (ap_weakly_constant (λa, ap g (p a)) q) + (ap_compose g f q)⁻¹ + (!ap_con ⬝ whisker_left _ !ap_inv) := + begin + induction q, esimp, generalize (p x), intro p, cases p, apply ids +-- induction q, rewrite [↑ap_compose,ap_inv], apply hinverse, apply ap_con_right_inv_sq, + end + + theorem ap_ap_compose {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) + {x y : A} (p : x = y) : + square (ap_compose (h ∘ g) f p) + (ap (ap h) (ap_compose g f p)) + (ap_compose h (g ∘ f) p) + (ap_compose h g (ap f p)) := + by induction p;exact ids + + theorem ap_compose_inv {A B C : Type} (g : B → C) (f : A → B) + {x y : A} (p : x = y) : + square (ap_compose g f p⁻¹) + (inverse2 (ap_compose g f p) ⬝ (ap_inv g (ap f p))⁻¹) + (ap_inv (g ∘ f) p) + (ap (ap g) (ap_inv f p)) := + by induction p;exact ids + + theorem ap_compose_con (g : B → C) (f : A → B) (p : a₁ = a₂) (q : a₂ = a₃) : + square (ap_compose g f (p ⬝ q)) + (ap_compose g f p ◾ ap_compose g f q ⬝ (ap_con g (ap f p) (ap f q))⁻¹) + (ap_con (g ∘ f) p q) + (ap (ap g) (ap_con f p q)) := + by induction q;induction p;exact ids + + theorem ap_compose_natural {A B C : Type} (g : B → C) (f : A → B) + {x y : A} {p q : x = y} (r : p = q) : + square (ap (ap (g ∘ f)) r) + (ap (ap g ∘ ap f) r) + (ap_compose g f p) + (ap_compose g f q) := + natural_square (ap_compose g f) r + +-- definition naturality_apdo {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} +-- (H : f ~ g) (p : a = a₂) +-- : squareover B vrfl (apdo f p) (apdo g p) +-- (pathover_idp_of_eq (H a)) (pathover_idp_of_eq (H a₂)) := +-- by induction p;esimp;exact hrflo + +definition naturality_apdo_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} + (H : f ~ g) (p : a = a₂) + : apdo f p = concato_eq (eq_concato (H a) (apdo g p)) (H a₂)⁻¹ := +begin + induction p, esimp, + generalizes [H a, g a], intro ga Ha, induction Ha, + reflexivity +end + +end eq