From ea0f57aef53b8fe2d29a286fde31d9e3ee49dc3c Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 23 Jun 2015 12:47:52 -0400 Subject: [PATCH] feat(hott): various clean-up and small additions --- hott/arity.hlean | 20 +- hott/hit/sphere.hlean | 18 +- hott/hit/susp.hlean | 22 +-- hott/init/equiv.hlean | 12 +- hott/init/funext.hlean | 17 +- hott/init/hit.hlean | 2 +- hott/init/path.hlean | 84 ++++----- hott/init/pathover.hlean | 84 ++++++--- hott/types/cubical/cubical.md | 8 +- hott/types/cubical/default.hlean | 1 - hott/types/cubical/pathover.hlean | 50 ----- hott/types/cubical/square.hlean | 273 ++++++++++++++++++++-------- hott/types/cubical/squareover.hlean | 66 ++++++- hott/types/eq.hlean | 128 +++++++------ hott/types/pointed.hlean | 26 +-- hott/types/sigma.hlean | 53 +++--- src/emacs/lean-input.el | 7 +- src/emacs/lean-syntax.el | 2 +- 18 files changed, 532 insertions(+), 341 deletions(-) delete mode 100644 hott/types/cubical/pathover.hlean diff --git a/hott/arity.hlean b/hott/arity.hlean index e982bcfa8..8d19e009a 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -121,10 +121,10 @@ namespace eq -- : f a b c d e ff g h = f a' b' c' d' e' f' g' h' := -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity - definition apd100 {f g : Πa b, C a b} (p : f = g) : f ~2 g := + definition apd100 [unfold-c 6] {f g : Πa b, C a b} (p : f = g) : f ~2 g := λa b, apd10 (apd10 p a) b - definition apd1000 {f g : Πa b c, D a b c} (p : f = g) : f ~3 g := + definition apd1000 [unfold-c 7] {f g : Πa b c, D a b c} (p : f = g) : f ~3 g := λa b c, apd100 (apd10 p a) b c /- some properties of these variants of ap -/ @@ -163,6 +163,22 @@ namespace eq apply eq_of_homotopy_idp end + definition eq_of_homotopy2_inv {f g : Πa b, C a b} (H : f ~2 g) + : eq_of_homotopy2 (λa b, (H a b)⁻¹) = (eq_of_homotopy2 H)⁻¹ := + ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy_inv)) ⬝ !eq_of_homotopy_inv + + definition eq_of_homotopy3_inv {f g : Πa b c, D a b c} (H : f ~3 g) + : eq_of_homotopy3 (λa b c, (H a b c)⁻¹) = (eq_of_homotopy3 H)⁻¹ := + ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy2_inv)) ⬝ !eq_of_homotopy_inv + + definition eq_of_homotopy2_con {f g h : Πa b, C a b} (H1 : f ~2 g) (H2 : g ~2 h) + : eq_of_homotopy2 (λa b, H1 a b ⬝ H2 a b) = eq_of_homotopy2 H1 ⬝ eq_of_homotopy2 H2 := + ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy_con)) ⬝ !eq_of_homotopy_con + + definition eq_of_homotopy3_con {f g h : Πa b c, D a b c} (H1 : f ~3 g) (H2 : g ~3 h) + : eq_of_homotopy3 (λa b c, H1 a b c ⬝ H2 a b c) = eq_of_homotopy3 H1 ⬝ eq_of_homotopy3 H2 := + ap eq_of_homotopy (eq_of_homotopy (λa, !eq_of_homotopy2_con)) ⬝ !eq_of_homotopy_con + end eq open eq is_equiv diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean index 63482382c..8fa9bb2af 100644 --- a/hott/hit/sphere.hlean +++ b/hott/hit/sphere.hlean @@ -100,10 +100,10 @@ namespace sphere nat.rec_on n (by esimp [Iterated_loop_space]; exact base) (by intro n s;exact apn n (equator n) s) - definition bool_of_sphere [reducible] : S 0 → bool := + definition bool_of_sphere : S 0 → bool := susp.rec ff tt (λx, empty.elim x) - definition sphere_of_bool [reducible] : bool → S 0 + definition sphere_of_bool : bool → S 0 | ff := north | tt := south @@ -124,17 +124,17 @@ namespace sphere revert A, induction n with n IH, { intro A, rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv}, { intro A, transitivity _, apply susp_adjoint_loop (S. n) A, apply IH} - end + end -- can we prove this in such a way that the function from left to right is apn _ surf? protected definition elim {n : ℕ} {P : Pointed} (p : Ω[n] P) : map₊ (S. n) P := to_inv !pmap_sphere p - definition elim_surf {n : ℕ} {P : Pointed} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := - begin - induction n with n IH, - { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry}, - { apply sorry} - end + -- definition elim_surf {n : ℕ} {P : Pointed} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := + -- begin + -- induction n with n IH, + -- { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry}, + -- { apply sorry} + -- end end sphere diff --git a/hott/hit/susp.hlean b/hott/hit/susp.hlean index 3b456666a..1753b1a7a 100644 --- a/hott/hit/susp.hlean +++ b/hott/hit/susp.hlean @@ -90,7 +90,7 @@ namespace susp definition Susp_functor (f : X →* Y) : Susp X →* Susp Y := begin - constructor, + fconstructor, { intro x, induction x, apply north, apply south, @@ -101,12 +101,12 @@ namespace susp definition Susp_functor_compose (g : Y →* Z) (f : X →* Y) : Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f := begin - constructor, + fconstructor, { intro a, induction a, { reflexivity}, { reflexivity}, { apply pathover_eq, apply hdeg_square, - rewrite [▸*,ap_compose' (Susp_functor f),↑Susp_functor,+elim_merid]}}, + rewrite [▸*,ap_compose' _ (Susp_functor f),↑Susp_functor,+elim_merid]}}, { reflexivity} end @@ -114,7 +114,7 @@ namespace susp definition loop_susp_unit [constructor] (X : Pointed) : X →* Ω(Susp X) := begin - constructor, + fconstructor, { intro x, exact merid x ⬝ (merid pt)⁻¹}, { apply con.right_inv}, end @@ -123,7 +123,7 @@ namespace susp : loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - constructor, + fconstructor, { intro x', esimp [Susp_functor], symmetry, exact !idp_con ⬝ @@ -141,7 +141,7 @@ namespace susp definition loop_susp_counit [constructor] (X : Pointed) : Susp (Ω X) →* X := begin - constructor, + fconstructor, { intro x, induction x, exact pt, exact pt, exact a}, { reflexivity}, end @@ -150,12 +150,12 @@ namespace susp : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (Susp_functor (ap1 f)) := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, - constructor, + fconstructor, { intro x', induction x' with p, { reflexivity}, { reflexivity}, { esimp, apply pathover_eq, apply hdeg_square, - xrewrite [ap_compose _ f,ap_compose _ (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*, + xrewrite [ap_compose f,ap_compose (susp.elim (f x) (f x) (λ (a : f x = f x), a)),▸*, +elim_merid,▸*,idp_con]}}, { reflexivity} end @@ -163,7 +163,7 @@ namespace susp definition loop_susp_counit_unit (X : Pointed) : ap1 (loop_susp_counit X) ∘* loop_susp_unit (Ω X) ~* pid (Ω X) := begin - induction X with X x, constructor, + induction X with X x, fconstructor, { intro p, esimp, refine !idp_con ⬝ (!ap_con ⬝ @@ -177,12 +177,12 @@ namespace susp definition loop_susp_unit_counit (X : Pointed) : loop_susp_counit (Susp X) ∘* Susp_functor (loop_susp_unit X) ~* pid (Susp X) := begin - induction X with X x, constructor, + induction X with X x, fconstructor, { intro x', induction x', { reflexivity}, { exact merid pt}, { apply pathover_eq, - xrewrite [▸*, ap_id, ap_compose _ (susp.elim north north (λa, a)), +elim_merid,▸*], + xrewrite [▸*, ap_id, ap_compose (susp.elim north north (λa, a)), +elim_merid,▸*], apply square_of_eq, exact !idp_con ⬝ !inv_con_cancel_right⁻¹}}, { reflexivity} end diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 56fdbe300..dee5d611c 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -52,10 +52,10 @@ namespace is_equiv (λa, (whisker_left _ (adj g (f a))) ⬝ (ap_con g _ _)⁻¹ ⬝ ap02 g ((ap_con_eq_con (right_inv f) (left_inv g (f a)))⁻¹ ⬝ - (ap_compose (inv f) f _ ◾ adj f a) ⬝ + (ap_compose f (inv f) _ ◾ adj f a) ⬝ (ap_con f _ _)⁻¹ ) ⬝ - (ap_compose f g _)⁻¹ + (ap_compose g f _)⁻¹ ) -- Any function equal to an equivalence is an equivlance as well. @@ -150,12 +150,12 @@ namespace is_equiv (λq, !ap_con ⬝ whisker_right !ap_con _ ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) - ◾ (inverse (ap_compose f⁻¹ f _)) + ◾ (inverse (ap_compose f f⁻¹ _)) ◾ (adj f _)⁻¹) ⬝ con_ap_con_eq_con_con (right_inv f) _ _ ⬝ whisker_right !con.left_inv _ ⬝ !idp_con) - (λp, whisker_right (whisker_left _ (ap_compose f f⁻¹ _)⁻¹) _ + (λp, whisker_right (whisker_left _ (ap_compose f⁻¹ f _)⁻¹) _ ⬝ con_ap_con_eq_con_con (left_inv f) _ _ ⬝ whisker_right !con.left_inv _ ⬝ !idp_con) @@ -278,8 +278,8 @@ namespace equiv theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ := eq.rec_on p idp - definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q - definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p + definition equiv_of_equiv_of_eq [trans] {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q + definition equiv_of_eq_of_equiv [trans] {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _ diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index ac6150f92..e54a6f047 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -231,7 +231,7 @@ definition funext_of_ua : funext := variables {A : Type} {P : A → Type} {f g : Π x, P x} namespace funext - definition is_equiv_apd [instance] (f g : Π x, P x) : is_equiv (@apd10 A P f g) := + theorem is_equiv_apd [instance] (f g : Π x, P x) : is_equiv (@apd10 A P f g) := funext_of_ua f g end funext @@ -261,3 +261,18 @@ right_inv apd10 p ▸ H (eq_of_homotopy p) protected definition homotopy.rec_on_idp [recursor] {Q : Π{g}, (f ~ g) → Type} {g : Π x, P x} (p : f ~ g) (H : Q (homotopy.refl f)) : Q p := homotopy.rec_on p (λq, eq.rec_on q H) + +definition eq_of_homotopy_inv {f g : Π x, P x} (H : f ~ g) + : eq_of_homotopy (λx, (H x)⁻¹) = (eq_of_homotopy H)⁻¹ := +begin + apply homotopy.rec_on_idp H, + rewrite [+eq_of_homotopy_idp] +end + +definition eq_of_homotopy_con {f g h : Π x, P x} (H1 : f ~ g) (H2 : g ~ h) + : eq_of_homotopy (λx, H1 x ⬝ H2 x) = eq_of_homotopy H1 ⬝ eq_of_homotopy H2 := +begin + apply homotopy.rec_on_idp H1, + apply homotopy.rec_on_idp H2, + rewrite [+eq_of_homotopy_idp] +end diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index da1fd0e3b..83bf7113c 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -51,7 +51,7 @@ namespace quotient constant class_of {A : Type} (R : A → A → Type) (a : A) : quotient R - constant eq_of_rel {A : Type} (R : A → A → Type) {a a' : A} (H : R a a') + constant eq_of_rel {A : Type} (R : A → A → Type) ⦃a a' : A⦄ (H : R a a') : class_of R a = class_of R a' protected constant rec {A : Type} {R : A → A → Type} {P : quotient R → Type} diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 72789880f..635dd68ac 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -46,11 +46,11 @@ namespace eq /- The 1-dimensional groupoid structure -/ -- The identity path is a right unit. - definition con_idp (p : x = y) : p ⬝ idp = p := - eq.rec_on p idp + definition con_idp [unfold-f] (p : x = y) : p ⬝ idp = p := + idp -- The identity path is a right unit. - definition idp_con (p : x = y) : idp ⬝ p = p := + definition idp_con [unfold-c 4] (p : x = y) : idp ⬝ p = p := eq.rec_on p idp -- Concatenation is associative. @@ -113,42 +113,42 @@ namespace eq p = r⁻¹ ⬝ q → r ⬝ p = q := eq.rec_on r (take p h, !idp_con ⬝ h ⬝ !idp_con) p - definition con_eq_of_eq_con_inv {p : x = z} {q : y = z} {r : y = x} : + definition con_eq_of_eq_con_inv [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : r = q ⬝ p⁻¹ → r ⬝ p = q := - eq.rec_on p (take q h, (!con_idp ⬝ h ⬝ !con_idp)) q + eq.rec_on p (take q h, h) q definition inv_con_eq_of_eq_con {p : x = z} {q : y = z} {r : x = y} : p = r ⬝ q → r⁻¹ ⬝ p = q := eq.rec_on r (take q h, !idp_con ⬝ h ⬝ !idp_con) q - definition con_inv_eq_of_eq_con {p : z = x} {q : y = z} {r : y = x} : + definition con_inv_eq_of_eq_con [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : r = q ⬝ p → r ⬝ p⁻¹ = q := - eq.rec_on p (take r h, !con_idp ⬝ h ⬝ !con_idp) r + eq.rec_on p (take r h, h) r definition eq_con_of_inv_con_eq {p : x = z} {q : y = z} {r : y = x} : r⁻¹ ⬝ q = p → q = r ⬝ p := eq.rec_on r (take p h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) p - definition eq_con_of_con_inv_eq {p : x = z} {q : y = z} {r : y = x} : + definition eq_con_of_con_inv_eq [unfold-c 5] {p : x = z} {q : y = z} {r : y = x} : q ⬝ p⁻¹ = r → q = r ⬝ p := - eq.rec_on p (take q h, !con_idp⁻¹ ⬝ h ⬝ !con_idp⁻¹) q + eq.rec_on p (take q h, h) q definition eq_inv_con_of_con_eq {p : x = z} {q : y = z} {r : x = y} : r ⬝ q = p → q = r⁻¹ ⬝ p := eq.rec_on r (take q h, !idp_con⁻¹ ⬝ h ⬝ !idp_con⁻¹) q - definition eq_con_inv_of_con_eq {p : z = x} {q : y = z} {r : y = x} : + definition eq_con_inv_of_con_eq [unfold-c 5] {p : z = x} {q : y = z} {r : y = x} : q ⬝ p = r → q = r ⬝ p⁻¹ := - eq.rec_on p (take r h, !con_idp⁻¹ ⬝ h ⬝ !con_idp⁻¹) r + eq.rec_on p (take r h, h) r - definition eq_of_con_inv_eq_idp {p q : x = y} : p ⬝ q⁻¹ = idp → p = q := - eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p + definition eq_of_con_inv_eq_idp [unfold-c 5] {p q : x = y} : p ⬝ q⁻¹ = idp → p = q := + eq.rec_on q (take p h, h) p definition eq_of_inv_con_eq_idp {p q : x = y} : q⁻¹ ⬝ p = idp → p = q := eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p - definition eq_inv_of_con_eq_idp' {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ := - eq.rec_on q (take p h, !con_idp⁻¹ ⬝ h) p + definition eq_inv_of_con_eq_idp' [unfold-c 5] {p : x = y} {q : y = x} : p ⬝ q = idp → p = q⁻¹ := + eq.rec_on q (take p h, h) p definition eq_inv_of_con_eq_idp {p : x = y} {q : y = x} : q ⬝ p = idp → p = q⁻¹ := eq.rec_on q (take p h, !idp_con⁻¹ ⬝ h) p @@ -156,11 +156,11 @@ namespace eq definition eq_of_idp_eq_inv_con {p q : x = y} : idp = p⁻¹ ⬝ q → p = q := eq.rec_on p (take q h, h ⬝ !idp_con) q - definition eq_of_idp_eq_con_inv {p q : x = y} : idp = q ⬝ p⁻¹ → p = q := - eq.rec_on p (take q h, h ⬝ !con_idp) q + definition eq_of_idp_eq_con_inv [unfold-c 4] {p q : x = y} : idp = q ⬝ p⁻¹ → p = q := + eq.rec_on p (take q h, h) q - definition inv_eq_of_idp_eq_con {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q := - eq.rec_on p (take q h, h ⬝ !con_idp) q + definition inv_eq_of_idp_eq_con [unfold-c 4] {p : x = y} {q : y = x} : idp = q ⬝ p → p⁻¹ = q := + eq.rec_on p (take q h, h) q definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q := eq.rec_on p (take q h, h ⬝ !idp_con) q @@ -214,8 +214,8 @@ namespace eq protected definition homotopy.symm [symm] [reducible] {f g : Πx, P x} (H : f ~ g) : g ~ f := λ x, (H x)⁻¹ - protected definition homotopy.trans [trans] [reducible] {f g h : Πx, P x} (H1 : f ~ g) (H2 : g ~ h) - : f ~ h := + protected definition homotopy.trans [trans] [reducible] {f g h : Πx, P x} + (H1 : f ~ g) (H2 : g ~ h) : f ~ h := λ x, H1 x ⬝ H2 x definition apd10 [unfold-c 5] {f g : Πx, P x} (H : f = g) : f ~ g := @@ -264,12 +264,12 @@ namespace eq ap f (p ⬝ q) = ap f p ⬝ ap f q := eq.rec_on q (eq.rec_on p idp) - definition con_ap_con_eq_con_ap_con_ap (f : A → B) {w x y z : A} (r : f w = f x) (p : x = y) (q : y = z) : - r ⬝ ap f (p ⬝ q) = (r ⬝ ap f p) ⬝ ap f q := - eq.rec_on q (take p, eq.rec_on p (con.assoc' r idp idp)) p + definition con_ap_con_eq_con_ap_con_ap (f : A → B) {w x y z : A} (r : f w = f x) + (p : x = y) (q : y = z) : r ⬝ ap f (p ⬝ q) = (r ⬝ ap f p) ⬝ ap f q := + eq.rec_on q (take p, eq.rec_on p idp) p - definition ap_con_con_eq_ap_con_ap_con (f : A → B) {w x y z : A} (p : x = y) (q : y = z) (r : f z = f w) : - ap f (p ⬝ q) ⬝ r = ap f p ⬝ (ap f q ⬝ r) := + definition ap_con_con_eq_ap_con_ap_con (f : A → B) {w x y z : A} (p : x = y) (q : y = z) + (r : f z = f w) : ap f (p ⬝ q) ⬝ r = ap f p ⬝ (ap f q ⬝ r) := eq.rec_on q (eq.rec_on p (take r, con.assoc _ _ _)) r -- Functions commute with path inverses. @@ -284,13 +284,12 @@ namespace eq definition ap_id (p : x = y) : ap id p = p := eq.rec_on p idp - -- TODO: interchange arguments f and g - definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x = y) : + definition ap_compose (g : B → C) (f : A → B) {x y : A} (p : x = y) : ap (g ∘ f) p = ap g (ap f p) := eq.rec_on p idp -- Sometimes we don't have the actual function [compose]. - definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x = y) : + definition ap_compose' (g : B → C) (f : A → B) {x y : A} (p : x = y) : ap (λa, g (f a)) p = ap g (ap f p) := eq.rec_on p idp @@ -448,7 +447,8 @@ namespace eq {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▸ b) := eq.rec_on p z - -- In Coq the variables P, Q and b are explicit, but in Lean we can probably have them implicit using the following notation + -- In Coq the variables P, Q and b are explicit, but in Lean we can probably have them implicit + -- using the following notation notation p `▸D`:65 x:64 := transportD _ p _ x -- Transporting along higher-dimensional paths @@ -482,7 +482,7 @@ namespace eq definition ap_tr_con_tr2 (P : A → Type) {x y : A} {p q : x = y} {z w : P x} (r : p = q) (s : z = w) : ap (transport P p) s ⬝ transport2 P r w = transport2 P r z ⬝ ap (transport P q) s := - eq.rec_on r (!con_idp ⬝ !idp_con⁻¹) + eq.rec_on r !idp_con⁻¹ definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) : @@ -548,12 +548,13 @@ namespace eq : p ⬝ q = p' ⬝ q' := eq.rec_on h (eq.rec_on h' idp) - infixl `◾`:75 := concat2 - -- 2-dimensional path inversion definition inverse2 [unfold-c 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := eq.rec_on h idp + infixl `◾`:75 := concat2 + postfix [parsing-only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it? + /- Whiskering -/ definition whisker_left (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r := @@ -573,7 +574,7 @@ namespace eq -- Whiskering and identity paths. definition whisker_right_idp_right {p q : x = y} (h : p = q) : - (con_idp p)⁻¹ ⬝ whisker_right h idp ⬝ con_idp q = h := + whisker_right h idp = h := eq.rec_on h (eq.rec_on p idp) definition whisker_right_idp_left (p : x = y) (q : y = z) : @@ -615,7 +616,7 @@ namespace eq ⬝ con.assoc' p (q ⬝ r) s ⬝ whisker_right (con.assoc' p q r) s = con.assoc' p q (r ⬝ s) ⬝ con.assoc' (p ⬝ q) r s := - eq.rec_on s (eq.rec_on r (eq.rec_on q (eq.rec_on p idp))) + 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) : @@ -624,16 +625,14 @@ namespace eq definition eckmann_hilton {x:A} (p q : idp = idp :> x = x) : p ⬝ q = q ⬝ p := (!whisker_right_idp_right ◾ !whisker_left_idp_left)⁻¹ - ⬝ (!con_idp ◾ !con_idp) - ⬝ (!idp_con ◾ !idp_con) + ⬝ whisker_left _ !idp_con ⬝ !whisker_right_con_whisker_left - ⬝ (!idp_con ◾ !idp_con)⁻¹ - ⬝ (!con_idp ◾ !con_idp)⁻¹ + ⬝ whisker_right !idp_con⁻¹ _ ⬝ (!whisker_left_idp_left ◾ !whisker_right_idp_right) -- The action of functions on 2-dimensional paths definition ap02 [unfold-c 8] (f : A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q := - eq.rec_on r idp + ap (ap f) r definition ap02_con (f : A → B) {x y : A} {p p' p'' : x = y} (r : p = p') (r' : p' = p'') : ap02 f (r ⬝ r') = ap02 f r ⬝ ap02 f r' := @@ -659,9 +658,4 @@ namespace eq ⬝ (whisker_right (tr2_con r1 r2 (f x))⁻¹ (apd f p3)) := eq.rec_on r2 (eq.rec_on r1 (eq.rec_on p1 idp)) - -- Naturality of [ap] with constant function over a loop - definition ap_eq_idp {f : A → B} {b : B} (p : Πx, f x = b) {x : A} (q : x = x) : - ap f q = idp := - cancel_right (ap_con_eq p q ⬝ !idp_con⁻¹) - end eq diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index c74ba3807..52ec74fc0 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -12,7 +12,7 @@ import .path .equiv open equiv is_equiv equiv.ops variables {A A' : Type} {B : A → Type} {C : Πa, B a → Type} - {a a₂ a₃ a₄ : A} {p : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} + {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄} {c : C a b} {c₂ : C a₂ b₂} @@ -32,13 +32,13 @@ namespace eq definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := by cases p; cases r; exact idpo - definition tr_eq_of_pathover (r : b =[p] b₂) : p ▸ b = b₂ := + definition tr_eq_of_pathover [unfold-c 8] (r : b =[p] b₂) : p ▸ b = b₂ := by cases r; exact idp - definition eq_tr_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := + definition eq_tr_of_pathover [unfold-c 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := by cases r; exact idp - definition pathover_equiv_tr_eq (p : a = a₂) (b : B a) (b₂ : B a₂) + definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂) : (b =[p] b₂) ≃ (p ▸ b = b₂) := begin fapply equiv.MK, @@ -48,7 +48,7 @@ namespace eq { intro r, cases r, apply idp}, end - definition pathover_equiv_eq_tr (p : a = a₂) (b : B a) (b₂ : B a₂) + definition pathover_equiv_eq_tr [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂) : (b =[p] b₂) ≃ (b = p⁻¹ ▸ b₂) := begin fapply equiv.MK, @@ -58,22 +58,16 @@ namespace eq { intro r, cases r, apply idp}, end - definition pathover_tr (p : a = a₂) (b : B a) : b =[p] p ▸ b := - pathover_of_tr_eq idp + definition pathover_tr [unfold-c 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b := + by cases p;exact idpo - definition tr_pathover (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := + definition tr_pathover [unfold-c 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := pathover_of_eq_tr idp - definition concato (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := - pathover.rec_on r₂ (pathover.rec_on r idpo) + definition concato [unfold-c 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := + pathover.rec_on r₂ r - definition concato_eq (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := - eq.rec_on q r - - definition eq_concato (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ := - eq.rec_on q (λr, r) r - - definition inverseo (r : b =[p] b₂) : b₂ =[p⁻¹] b := + definition inverseo [unfold-c 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b := pathover.rec_on r idpo definition apdo [unfold-c 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := @@ -82,8 +76,16 @@ namespace eq definition oap [unfold-c 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ := eq.rec_on p idpo + definition concato_eq [unfold-c 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := + eq.rec_on q r + + definition eq_concato [unfold-c 9] (q : b = b') (r : b' =[p] b₂) : b =[p] b₂ := + by induction q;exact r + -- infix `⬝` := concato infix `⬝o`:75 := concato + infix `⬝op`:75 := concato_eq + infix `⬝po`:75 := eq_concato -- postfix `⁻¹` := inverseo postfix `⁻¹ᵒ`:(max+10) := inverseo @@ -103,16 +105,12 @@ namespace eq (r ⬝o r₂) ⬝o r₃ =[!con.assoc] r ⬝o (r₂ ⬝o r₃) := pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo)) - -- the left inverse law. definition cono.right_inv (r : b =[p] b₂) : r ⬝o r⁻¹ᵒ =[!con.right_inv] idpo := pathover.rec_on r idpo - -- the right inverse law. definition cono.left_inv (r : b =[p] b₂) : r⁻¹ᵒ ⬝o r =[!con.left_inv] idpo := pathover.rec_on r idpo - /- Some of the theorems analogous to theorems for transport in init.path -/ - definition eq_of_pathover {a' a₂' : A'} (q : a' =[p] a₂') : a' = a₂' := by cases q;reflexivity @@ -128,14 +126,28 @@ namespace eq { intro r, cases r, exact idp}, end - definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := - pathover_equiv_tr_eq idp b b' - - definition eq_of_pathover_idp {b' : B a} (q : b =[idpath a] b') : b = b' := + definition eq_of_pathover_idp [unfold-c 6] {b' : B a} (q : b =[idpath a] b') : b = b' := tr_eq_of_pathover q - definition pathover_idp_of_eq {b' : B a} (q : b = b') : b =[idpath a] b' := - pathover_of_tr_eq q + --should B be explicit in the next two definitions? + definition pathover_idp_of_eq [unfold-c 6] {b' : B a} (q : b = b') : b =[idpath a] b' := + eq.rec_on q idpo + + definition pathover_idp [constructor] (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := + equiv.MK eq_of_pathover_idp + (pathover_idp_of_eq) + (to_right_inv !pathover_equiv_tr_eq) + (to_left_inv !pathover_equiv_tr_eq) + + + -- definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := + -- pathover_equiv_tr_eq idp b b' + + -- definition eq_of_pathover_idp [reducible] {b' : B a} (q : b =[idpath a] b') : b = b' := + -- to_fun !pathover_idp q + + -- definition pathover_idp_of_eq [reducible] {b' : B a} (q : b = b') : b =[idpath a] b' := + -- to_inv !pathover_idp q definition idp_rec_on [recursor] {P : Π⦃b₂ : B a⦄, b =[idpath a] b₂ → Type} {b₂ : B a} (r : b =[idpath a] b₂) (H : P idpo) : P r := @@ -209,5 +221,23 @@ namespace eq {b : B a} : f b =[apo011 C p !pathover_tr] g (p ▸ b) := by cases r; exact idpo + definition cono.right_inv_eq (q : b = b') + : concato_eq (pathover_idp_of_eq q) q⁻¹ = (idpo : b =[refl a] b) := + by induction q;constructor + + definition cono.right_inv_eq' (q : b = b') + : eq_concato q (pathover_idp_of_eq q⁻¹) = (idpo : b =[refl a] b) := + by induction q;constructor + + definition cono.left_inv_eq (q : b = b') + : concato_eq (pathover_idp_of_eq q⁻¹) q = (idpo : b' =[refl a] b') := + by induction q;constructor + + definition cono.left_inv_eq' (q : b = b') + : eq_concato q⁻¹ (pathover_idp_of_eq q) = (idpo : b' =[refl a] b') := + by induction q;constructor + + definition change_path (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ := + by induction q;exact r end eq diff --git a/hott/types/cubical/cubical.md b/hott/types/cubical/cubical.md index 5633661bd..47bbd7d7d 100644 --- a/hott/types/cubical/cubical.md +++ b/hott/types/cubical/cubical.md @@ -8,10 +8,4 @@ The files [path](../../init/path.hlean) and [pathover](../../init/pathover.hlean * [square](square.hlean): square in a type * [cube](cube.hlean): cube in a type * [squareover](squareover.hlean): square over a square -* [cubeover](cubeover.hlean): cube over a cube - -Characterizing equality/pathovers in cubical types - -For [eq](../eq.hlean) this is done in the [types/](../types.md) folder - -* [pathover](pathover.hlean) \ No newline at end of file +* [cubeover](cubeover.hlean): cube over a cube \ No newline at end of file diff --git a/hott/types/cubical/default.hlean b/hott/types/cubical/default.hlean index 2141b17f7..fbf7c846e 100644 --- a/hott/types/cubical/default.hlean +++ b/hott/types/cubical/default.hlean @@ -5,4 +5,3 @@ Authors: Floris van Doorn -/ import .square .cube .squareover .cubeover -import .pathover diff --git a/hott/types/cubical/pathover.hlean b/hott/types/cubical/pathover.hlean deleted file mode 100644 index 6789d904f..000000000 --- a/hott/types/cubical/pathover.hlean +++ /dev/null @@ -1,50 +0,0 @@ -/- -Copyright (c) 2015 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn - -Pathovers. -Note that the basic definitions are in init.pathover --/ - -import .squareover - -open eq equiv is_equiv equiv.ops - -namespace eq - - variables {A A' : Type} {B B' : A → Type} {C : Πa, B a → Type} - {a a₂ a₃ a₄ : A} {p : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄} - {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄} - {c : C a b} {c₂ : C a₂ b₂} - {q q' : a =[p] a₂} - - --in this version A' does not depend on A - definition pathover_pathover_fl {a' a₂' : A'} {p : a' = a₂'} {a₂ : A} {f : A' → A} - {b : Πa, B (f a)} {b₂ : B a₂} {q : Π(a' : A'), f a' = a₂} (r : pathover B (b a') (q a') b₂) - (r₂ : pathover B (b a₂') (q a₂') b₂) - (s : squareover B (natural_square q p) r r₂ (pathover_ap B f (apdo b p)) (!ap_constant⁻¹ ▸ idpo)) - : r =[p] r₂ := - by cases p; esimp at s; apply pathover_idp_of_eq; apply eq_of_vdeg_squareover; exact s - --- definition pathover_pathover {ba ba' : Πa, B a} {pa : Πa, ba a = ba a} --- {ca : Πa, C a (ba a)} {ca' : Πa, C a (ba' a)} --- {qa : ba a =[pa a] ba' a} {qa₂ : ba a₂ =[pa a₂] ba' a₂} --- (r : squareover _ _ _ _ _ _) : qa =[p] qa₂ := --- sorry - --- definition pathover_pathover_constant_FlFr {C : A → A' → Type} {ba ba' : A → A'} {pa : Πa, ba a = ba a} --- {ca : Πa, C a (ba a)} {ca' : Πa, C a (ba' a)} --- {qa : ba a =[pa a] ba' a} {qa₂ : ba a₂ =[pa a₂] ba' a₂} --- (r : squareover (λa, C a _) _ _ _ _ _) : pathover _ qa p qa₂ := sorry - --- definition pathover_pathover_constant_l {C : A → A' → Type} {ba ba' : A → A'} {pa : Πa, ba a = ba a} --- {ca : Πa, C a (ba a)} {ca' : Πa, C a (ba' a)} --- {qa : ba a =[pa a] ba' a} {qa₂ : ba a₂ =[pa a₂] ba' a₂} --- (r : squareover (λa, C a _) _ _ _ _ _) : qa =[p] qa₂ := --- begin --- check_expr qa =[p] qa₂ --- end - - -end eq diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean index 1d95aec40..357a95f5d 100644 --- a/hott/types/cubical/square.hlean +++ b/hott/types/cubical/square.hlean @@ -30,67 +30,120 @@ namespace eq definition idsquare [reducible] [constructor] (a : A) := @square.ids A a definition hrefl [unfold-c 4] (p : a = a') : square idp idp p p := - by cases p; exact ids + by induction p; exact ids definition vrefl [unfold-c 4] (p : a = a') : square p p idp idp := - by cases p; exact ids + by induction p; exact ids definition hrfl [unfold-c 4] {p : a = a'} : square idp idp p p := !hrefl definition vrfl [unfold-c 4] {p : a = a'} : square p p idp idp := !vrefl - definition hconcat (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) + definition hdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square idp idp p q := + by induction r;apply hrefl + + definition vdeg_square [unfold-c 6] {p q : a = a'} (r : p = q) : square p q idp idp := + by induction r;apply vrefl + + definition hconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ := - by cases s₃₁; exact s₁₁ + by induction s₃₁; exact s₁₁ - definition vconcat (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) + definition vconcat [unfold-c 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) : square p₁₀ p₁₄ (p₀₁ ⬝ p₀₃) (p₂₁ ⬝ p₂₃) := - by cases s₁₃; exact s₁₁ + by induction s₁₃; exact s₁₁ - definition hinverse (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := - by cases s₁₁;exact ids + definition hinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := + by induction s₁₁;exact ids - definition vinverse (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := - by cases s₁₁;exact ids + definition vinverse [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := + by induction s₁₁;exact ids - definition transpose (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := - by cases s₁₁;exact ids + definition eq_vconcat [unfold-c 11] {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + square p p₁₂ p₀₁ p₂₁ := + by induction r; exact s₁₁ - definition eq_of_square (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := - by cases s₁₁; apply idp + definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : + square p₁₀ p p₀₁ p₂₁ := + by induction r; exact s₁₁ - definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ := - by cases p₁₂; esimp [concat] at r; cases r; cases p₂₁; cases p₁₀; exact ids + definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + square p₁₀ p₁₂ p p₂₁ := + by induction r; exact s₁₁ + + definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : + square p₁₀ p₁₂ p₀₁ p := + by induction r; exact s₁₁ + + + infix `⬝h`:75 := hconcat + infix `⬝v`:75 := vconcat + infix `⬝hp`:75 := hconcat_eq + infix `⬝vp`:75 := vconcat_eq + infix `⬝ph`:75 := eq_hconcat + infix `⬝pv`:75 := eq_vconcat + postfix `⁻¹ʰ`:(max+1) := hinverse + postfix `⁻¹ᵛ`:(max+1) := vinverse + + definition transpose [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := + by induction s₁₁;exact ids definition aps {B : Type} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square (ap f p₁₀) (ap f p₁₂) (ap f p₀₁) (ap f p₂₁) := - by cases s₁₁;exact ids + by induction s₁₁;exact ids - definition square_of_homotopy {B : Type} {f g : A → B} (H : f ~ g) (p : a = a') - : square (H a) (H a') (ap f p) (ap g p) := - by cases p; apply vrefl + definition natural_square [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : + square (ap f q) (ap g q) (p a) (p a') := + eq.rec_on q hrfl - definition square_of_homotopy' {B : Type} {f g : A → B} (H : f ~ g) (p : a = a') - : square (ap f p) (ap g p) (H a) (H a') := - by cases p; apply hrefl + definition natural_square_tr [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : + square (p a) (p a') (ap f q) (ap g q) := + eq.rec_on q vrfl - definition square_equiv_eq (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂) (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂) - : square t b l r ≃ t ⬝ r = l ⬝ b := + definition whisker_tl (p : a = a₀₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square (p ⬝ p₁₀) p₁₂ (p ⬝ p₀₁) p₂₁ := + by induction s₁₁;induction p;exact ids + + definition whisker_br (p : a₂₂ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : square p₁₀ (p₁₂ ⬝ p) p₀₁ (p₂₁ ⬝ p) := + by induction p;exact s₁₁ + + /- some higher ∞-groupoid operations -/ + + definition vconcat_vrfl (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : s₁₁ ⬝v vrefl p₁₂ = s₁₁ := + by induction s₁₁; reflexivity + + definition hconcat_hrfl (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : s₁₁ ⬝h hrefl p₂₁ = s₁₁ := + by induction s₁₁; reflexivity + + /- equivalences -/ + + definition eq_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := + by induction s₁₁; apply idp + + definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids + + definition eq_top_of_square [unfold-c 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ := + by induction s₁₁; apply idp + + definition square_of_eq_top (r : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹) : square p₁₀ p₁₂ p₀₁ p₂₁ := + by induction p₂₁; induction p₁₂; esimp at r;induction r;induction p₁₀;exact ids + + definition square_equiv_eq [constructor] (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂) + (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂) : square t b l r ≃ t ⬝ r = l ⬝ b := begin fapply equiv.MK, { exact eq_of_square}, { exact square_of_eq}, - { intro s, cases b, esimp [concat] at s, cases s, cases r, cases t, apply idp}, - { intro s, cases s, apply idp}, + { intro s, induction b, esimp [concat] at s, induction s, induction r, induction t, apply idp}, + { intro s, induction s, apply idp}, end - definition hdeg_square {p q : a = a'} (r : p = q) : square idp idp p q := - by cases r;apply hrefl - - definition vdeg_square {p q : a = a'} (r : p = q) : square p q idp idp := - by cases r;apply vrefl - definition hdeg_square_equiv' [constructor] (p q : a = a') : square idp idp p q ≃ p = q := by transitivity _;apply square_equiv_eq;transitivity _;apply eq_equiv_eq_symm; apply equiv_eq_closed_right;apply idp_con @@ -106,13 +159,14 @@ namespace eq /- the following two equivalences have as underlying inverse function the functions - hdeg_square and vdeg_square, respectively + hdeg_square and vdeg_square, respectively. + See examples below the definition -/ definition hdeg_square_equiv [constructor] (p q : a = a') : square idp idp p q ≃ p = q := begin fapply equiv_change_fun, { fapply equiv_change_inv, apply hdeg_square_equiv', exact hdeg_square, - intro s, cases s, cases p, reflexivity}, + intro s, induction s, induction p, reflexivity}, { exact eq_of_hdeg_square}, { reflexivity} end @@ -121,7 +175,7 @@ namespace eq begin fapply equiv_change_fun, { fapply equiv_change_inv, apply vdeg_square_equiv',exact vdeg_square, - intro s, cases s, cases p, reflexivity}, + intro s, induction s, induction p, reflexivity}, { exact eq_of_vdeg_square}, { reflexivity} end @@ -129,16 +183,110 @@ namespace eq -- example (p q : a = a') : to_inv (hdeg_square_equiv' p q) = hdeg_square := idp -- this fails example (p q : a = a') : to_inv (hdeg_square_equiv p q) = hdeg_square := idp - definition natural_square [unfold-c 8] {f g : A → B} (p : f ~ g) (q : a = a') : - square (p a) (p a') (ap f q) (ap g q) := - eq.rec_on q vrfl + definition pathover_eq [unfold-c 7] {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} + (s : square q r (ap f p) (ap g p)) : q =[p] r := + by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s + + definition square_of_pathover [unfold-c 7] + {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} + (s : q =[p] r) : square q r (ap f p) (ap g p) := + by induction p;apply vdeg_square;exact eq_of_pathover_idp s + + /- interaction of equivalences with operations on squares -/ + + definition pathover_eq_equiv_square [constructor] {f g : A → B} + (p : a = a') (q : f a = g a) (r : f a' = g a') : q =[p] r ≃ square q r (ap f p) (ap g p) := + equiv.MK square_of_pathover + pathover_eq + begin + intro s, induction p, esimp [square_of_pathover,pathover_eq], + exact ap vdeg_square (to_right_inv !pathover_idp (eq_of_vdeg_square s)) + ⬝ to_left_inv !vdeg_square_equiv s + end + begin + intro s, induction p, esimp [square_of_pathover,pathover_eq], + exact ap pathover_idp_of_eq (to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s)) + ⬝ to_left_inv !pathover_idp s + end + + definition square_of_pathover_eq_concato {f g : A → B} {p : a = a'} {q q' : f a = g a} + {r : f a' = g a'} (s' : q = q') (s : q' =[p] r) + : square_of_pathover (s' ⬝po s) = s' ⬝pv square_of_pathover s := + by induction s;induction s';reflexivity + + definition square_of_pathover_concato_eq {f g : A → B} {p : a = a'} {q : f a = g a} + {r r' : f a' = g a'} (s' : r = r') (s : q =[p] r) + : square_of_pathover (s ⬝op s') = square_of_pathover s ⬝vp s' := + by induction s;induction s';reflexivity + + definition square_of_pathover_concato {f g : A → B} {p : a = a'} {p' : a' = a''} {q : f a = g a} + {q' : f a' = g a'} {q'' : f a'' = g a''} (s : q =[p] q') (s' : q' =[p'] q'') + : square_of_pathover (s ⬝o s') + = ap_con f p p' ⬝ph (square_of_pathover s ⬝v square_of_pathover s') ⬝hp (ap_con g p p')⁻¹ := + by induction s';induction s;esimp [ap_con,hconcat_eq];exact !vconcat_vrfl⁻¹ + + definition eq_of_square_hdeg_square {p q : a = a'} (r : p = q) + : eq_of_square (hdeg_square r) = !idp_con ⬝ r⁻¹ := + by induction r;induction p;reflexivity + + definition eq_of_square_vdeg_square {p q : a = a'} (r : p = q) + : eq_of_square (vdeg_square r) = r ⬝ !idp_con⁻¹ := + 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₁₁ := + 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₁₂)⁻¹ := + by induction r;reflexivity + + definition eq_of_square_vconcat_eq {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) + : eq_of_square (s₁₁ ⬝vp r) = eq_of_square s₁₁ ⬝ whisker_left p₀₁ r := + by induction r;reflexivity + + definition eq_of_square_hconcat_eq {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) + : eq_of_square (s₁₁ ⬝hp r) = (whisker_left p₁₀ r)⁻¹ ⬝ eq_of_square s₁₁ := + by induction s₁₁; induction r;reflexivity + + + -- definition vconcat_eq [unfold-c 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) : + -- square p₁₀ p p₀₁ p₂₁ := + -- by induction r; exact s₁₁ + + -- definition eq_hconcat [unfold-c 11] {p : a₀₀ = a₀₂} (r : p = p₀₁) + -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀ p₁₂ p p₂₁ := + -- by induction r; exact s₁₁ + + -- definition hconcat_eq [unfold-c 11] {p : a₂₀ = a₂₂} + -- (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) : square p₁₀ p₁₂ p₀₁ p := + -- by induction r; exact s₁₁ + + + -- the following definition is very slow, maybe it's interesting to see why? + -- definition pathover_eq_equiv_square' {f g : A → B}(p : a = a') (q : f a = g a) (r : f a' = g a') + -- : square q r (ap f p) (ap g p) ≃ q =[p] r := + -- equiv.MK pathover_eq + -- square_of_pathover + -- (λs, begin + -- induction p, rewrite [↑[square_of_pathover,pathover_eq], + -- to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s), + -- to_left_inv !pathover_idp s] + -- end) + -- (λs, begin + -- induction p, rewrite [↑[square_of_pathover,pathover_eq],▸*, + -- to_right_inv !(@pathover_idp A) (eq_of_vdeg_square s), + -- to_left_inv !vdeg_square_equiv s] + -- end) + + /- recursors for squares where some sides are reflexivity -/ definition rec_on_b [recursor] {a₀₀ : A} {P : Π{a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂}, square t idp l r → Type} {a₂₀ a₁₂ : A} {t : a₀₀ = a₂₀} {l : a₀₀ = a₁₂} {r : a₂₀ = a₁₂} (s : square t idp l r) (H : P ids) : P s := have H2 : P (square_of_eq (eq_of_square s)), - from eq.rec_on (eq_of_square s : t ⬝ r = l) (by cases r; cases t; exact H), + from eq.rec_on (eq_of_square s : t ⬝ r = l) (by induction r; induction t; exact H), left_inv (to_fun !square_equiv_eq) s ▸ H2 definition rec_on_r [recursor] {a₀₀ : A} @@ -147,7 +295,7 @@ namespace eq (s : square t b l idp) (H : P ids) : P s := let p : l ⬝ b = t := (eq_of_square s)⁻¹ in have H2 : P (square_of_eq (eq_of_square s)⁻¹⁻¹), - from @eq.rec_on _ _ (λx p, P (square_of_eq p⁻¹)) _ p (by cases b; cases l; exact H), + from @eq.rec_on _ _ (λx p, P (square_of_eq p⁻¹)) _ p (by induction b; induction l; exact H), left_inv (to_fun !square_equiv_eq) s ▸ !inv_inv ▸ H2 definition rec_on_l [recursor] {a₀₁ : A} @@ -157,7 +305,7 @@ namespace eq (s : square t b idp r) (H : P ids) : P s := let p : t ⬝ r = b := eq_of_square s ⬝ !idp_con in have H2 : P (square_of_eq (p ⬝ !idp_con⁻¹)), - from eq.rec_on p (by cases r; cases t; exact H), + from eq.rec_on p (by induction r; induction t; exact H), left_inv (to_fun !square_equiv_eq) s ▸ !con_inv_cancel_right ▸ H2 definition rec_on_t [recursor] {a₁₀ : A} @@ -166,7 +314,7 @@ namespace eq (s : square idp b l r) (H : P ids) : P s := let p : l ⬝ b = r := (eq_of_square s)⁻¹ ⬝ !idp_con in assert H2 : P (square_of_eq ((p ⬝ !idp_con⁻¹)⁻¹)), - from eq.rec_on p (by cases b; cases l; exact H), + from eq.rec_on p (by induction b; induction l; exact H), assert H3 : P (square_of_eq ((eq_of_square s)⁻¹⁻¹)), from eq.rec_on !con_inv_cancel_right H2, assert H4 : P (square_of_eq (eq_of_square s)), @@ -180,7 +328,7 @@ namespace eq {b : A} {l : a = b} {r : a = b} (s : square idp idp l r) (H : P ids) : P s := have H2 : P (square_of_eq (eq_of_square s)), - from eq.rec_on (eq_of_square s : idp ⬝ r = l) (by cases r; exact H), + from eq.rec_on (eq_of_square s : idp ⬝ r = l) (by induction r; exact H), left_inv (to_fun !square_equiv_eq) s ▸ H2 definition rec_on_lr [recursor] {a : A} @@ -189,44 +337,9 @@ namespace eq (s : square t b idp idp) (H : P ids) : P s := let p : idp ⬝ b = t := (eq_of_square s)⁻¹ in assert H2 : P (square_of_eq (eq_of_square s)⁻¹⁻¹), - from @eq.rec_on _ _ (λx q, P (square_of_eq q⁻¹)) _ p (by cases b; exact H), + from @eq.rec_on _ _ (λx q, P (square_of_eq q⁻¹)) _ p (by induction b; exact H), to_left_inv (!square_equiv_eq) s ▸ !inv_inv ▸ H2 --we can also do the other recursors (tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed - definition pathover_eq {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} - (s : square q r (ap f p) (ap g p)) : q =[p] r := - by cases p;apply pathover_idp_of_eq;exact eq_of_vdeg_square s - - definition square_of_pathover {f g : A → B} {p : a = a'} {q : f a = g a} {r : f a' = g a'} - (s : q =[p] r) : square q r (ap f p) (ap g p) := - by cases p;apply vdeg_square;exact eq_of_pathover_idp s -exit - definition pathover_eq_equiv_square {f g : A → B} (p : a = a') (q : f a = g a) (r : f a' = g a') - : square q r (ap f p) (ap g p) ≃ q =[p] r := - equiv.MK pathover_eq - square_of_pathover - (λs, begin cases p, esimp [square_of_pathover,pathover_eq], - let H := to_right_inv !vdeg_square_equiv (eq_of_pathover_idp s), - esimp at H, - rewrite [H] end - ) - (λs, by cases p;esimp [square_of_pathover,pathover_eq] at *) - - - -- set_option pp.notation false - -- set_option pp.implicit true -example {f g : A → B} (q : f a = g a) (r : f a = g a) (s : q =[idp] r) : - function.compose (to_fun (vdeg_square_equiv q r)) (to_fun (vdeg_square_equiv q r))⁻¹ - (eq_of_pathover_idp s) = sorry := - begin - esimp - end - -example {f g : A → B} (q : f a = g a) (r : f a = g a) (s : square q r idp idp) : - to_fun (vdeg_square_equiv q r) s = eq_of_vdeg_square s := - begin - - end - end eq diff --git a/hott/types/cubical/squareover.hlean b/hott/types/cubical/squareover.hlean index e05bd128a..21a7f841d 100644 --- a/hott/types/cubical/squareover.hlean +++ b/hott/types/cubical/squareover.hlean @@ -51,13 +51,73 @@ namespace eq square.rec_on s idso definition vrflo : squareover B vrfl q₁₀ q₁₀ idpo idpo := - by cases q₁₀; exact idso + by induction q₁₀; exact idso - definition vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (p : q₁₀ = q₁₀') + definition hrflo : squareover B hrfl idpo idpo q₁₀ q₁₀ := + by induction q₁₀; exact idso + + definition vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀') : squareover B vrfl q₁₀ q₁₀' idpo idpo := - by cases p;exact vrflo + by induction r;exact vrflo + + definition hdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀') + : squareover B hrfl idpo idpo q₁₀ q₁₀' := + by induction r; exact hrflo + + definition pathover_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) + : q₁₀ ⬝o q₂₁ =[eq_of_square s₁₁] q₀₁ ⬝o q₁₂ := + by induction t₁₁; constructor + + definition squareover_of_pathover {s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} + (r : q₁₀ ⬝o q₂₁ =[s] q₀₁ ⬝o q₁₂) : squareover B (square_of_eq s) q₁₀ q₁₂ q₀₁ q₂₁ := + by induction q₁₂; esimp [concato] at r;induction r;induction q₂₁;induction q₁₀;constructor + + definition pathover_top_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) + : q₁₀ =[eq_top_of_square s₁₁] q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ := + by induction t₁₁; constructor + + definition squareover_of_pathover_top {s : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹} + (r : q₁₀ =[s] q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ) + : squareover B (square_of_eq_top s) q₁₀ q₁₂ q₀₁ q₂₁ := + by induction q₂₁; induction q₁₂; esimp at r;induction r;induction q₁₀;constructor + + definition squareover_equiv_pathover (q₁₀ : b₀₀ =[p₁₀] b₂₀) (q₁₂ : b₀₂ =[p₁₂] b₂₂) + (q₀₁ : b₀₀ =[p₀₁] b₀₂) (q₂₁ : b₂₀ =[p₂₁] b₂₂) + : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ ≃ q₁₀ ⬝o q₂₁ =[eq_of_square s₁₁] q₀₁ ⬝o q₁₂ := + begin + fapply equiv.MK, + { exact pathover_of_squareover}, + { intro r, rewrite [-to_left_inv !square_equiv_eq s₁₁], apply squareover_of_pathover, exact r}, + { intro r, apply sorry}, --need characterization of squareover lying over ids. + { intro s, induction s, apply idp}, + end definition eq_of_vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (p : squareover B vrfl q₁₀ q₁₀' idpo idpo) : q₁₀ = q₁₀' := sorry + + -- definition vdeg_tr_squareover {q₁₂ : p₀₁ ▸ b₀₀ =[p₁₂] p₂₁ ▸ b₂₀} (r : q₁₀ =[_] q₁₂) + -- : squareover B s₁₁ q₁₀ q₁₂ !pathover_tr !pathover_tr := + -- by induction p;exact vrflo + + /- charcaterization of pathovers in pathovers -/ + -- in this version the fibration (B) of the pathover does not depend on the variable a + definition pathover_pathover {a' a₂' : A'} {p : a' = a₂'} {f g : A' → A} + {b : Πa, B (f a)} {b₂ : Πa, B (g a)} {q : Π(a' : A'), f a' = g a'} + (r : pathover B (b a') (q a') (b₂ a')) + (r₂ : pathover B (b a₂') (q a₂') (b₂ a₂')) + (s : squareover B (natural_square_tr q p) r r₂ + (pathover_ap B f (apdo b p)) (pathover_ap B g (apdo b₂ p))) + : pathover (λa, pathover B (b a) (q a) (b₂ a)) r p r₂ := + by induction p;esimp at s; apply pathover_idp_of_eq; apply eq_of_vdeg_squareover; exact s + + -- TODO: remove + definition pathover_pathover_fl {a' a₂' : A'} {p : a' = a₂'} {a₂ : A} {f : A' → A} + {b : Πa, B (f a)} {b₂ : B a₂} {q : Π(a' : A'), f a' = a₂} (r : pathover B (b a') (q a') b₂) + (r₂ : pathover B (b a₂') (q a₂') b₂) + (s : squareover B (natural_square_tr q p) r r₂ + (pathover_ap B f (apdo b p)) (change_path !ap_constant⁻¹ idpo)) + : r =[p] r₂ := + by induction p; esimp at s; apply pathover_idp_of_eq; apply eq_of_vdeg_squareover; exact s + end eq diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 769785105..53e1c8b1c 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -25,51 +25,67 @@ namespace eq theorem whisker_left_con_right (p : a1 = a2) {q q' q'' : a2 = a3} (r : q = q') (s : q' = q'') : whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s := begin - cases p, cases r, cases s, reflexivity + induction p, induction r, induction s, reflexivity end theorem whisker_right_con_right (q : a2 = a3) (r : p = p') (s : p' = p'') : whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q := begin - cases q, cases r, cases s, reflexivity + 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') : whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' := begin - cases p', cases p, cases r, cases q, reflexivity + 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') : whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc := begin - cases q', cases q, cases r, cases p, reflexivity + 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') : !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r := begin - cases p, cases r, cases q, reflexivity + induction p, induction r, induction q, reflexivity end + theorem whisker_left_inv (p : a1 = a2) {q q' : a2 = a3} (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') + : whisker_right r⁻¹ q = (whisker_right r q)⁻¹ := + by induction r; reflexivity + theorem ap_eq_ap10 {f g : A → B} (p : f = g) (a : A) : ap (λh, h a) p = ap10 p a := - by cases p;reflexivity + by induction p;reflexivity theorem inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p := - by cases r;cases p;reflexivity + by induction r;induction p;reflexivity theorem inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p := - by cases r;cases p;reflexivity + by induction r;induction p;reflexivity theorem ap_con_right_inv (f : A → B) (p : a1 = a2) : 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 cases p;reflexivity + by induction p;reflexivity theorem ap_con_left_inv (f : A → B) (p : a1 = a2) : 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 cases p;reflexivity + by induction p;reflexivity + + theorem idp_con_whisker_left {q q' : a2 = a3} (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') : + 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 @@ -85,40 +101,40 @@ namespace eq definition transport_eq_l (p : a1 = a2) (q : a1 = a3) : transport (λx, x = a3) p q = p⁻¹ ⬝ q := - by cases p; cases q; reflexivity + by induction p; induction q; reflexivity definition transport_eq_r (p : a2 = a3) (q : a1 = a2) : transport (λx, a1 = x) p q = q ⬝ p := - by cases p; cases q; reflexivity + by induction p; induction q; reflexivity definition transport_eq_lr (p : a1 = a2) (q : a1 = a1) : transport (λx, x = x) p q = p⁻¹ ⬝ q ⬝ p := - by cases p; rewrite [▸*,idp_con] + by induction p; rewrite [▸*,idp_con] definition transport_eq_Fl (p : a1 = a2) (q : f a1 = b) : transport (λx, f x = b) p q = (ap f p)⁻¹ ⬝ q := - by cases p; cases q; reflexivity + by induction p; induction q; reflexivity definition transport_eq_Fr (p : a1 = a2) (q : b = f a1) : transport (λx, b = f x) p q = q ⬝ (ap f p) := - by cases p; reflexivity + by induction p; reflexivity definition transport_eq_FlFr (p : a1 = a2) (q : f a1 = g a1) : transport (λx, f x = g x) p q = (ap f p)⁻¹ ⬝ q ⬝ (ap g p) := - by cases p; rewrite [▸*,idp_con] + 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) : transport (λx, f x = g x) p q = (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := - by cases p; rewrite [▸*,idp_con,ap_id] + by induction p; rewrite [▸*,idp_con,ap_id] definition transport_eq_FFlr (p : a1 = a2) (q : h (f a1) = a1) : transport (λx, h (f x) = x) p q = (ap h (ap f p))⁻¹ ⬝ q ⬝ p := - by cases p; rewrite [▸*,idp_con] + by induction p; rewrite [▸*,idp_con] definition transport_eq_lFFr (p : a1 = a2) (q : a1 = h (f a1)) : transport (λx, x = h (f x)) p q = p⁻¹ ⬝ q ⬝ (ap h (ap f p)) := - by cases p; rewrite [▸*,idp_con] + by induction p; rewrite [▸*,idp_con] /- Pathovers -/ @@ -128,44 +144,44 @@ namespace eq -- 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)-/ - by cases p; cases q; exact idpo + by induction p; induction q; exact idpo definition pathover_eq_r (p : a2 = a3) (q : a1 = a2) : q =[p] q ⬝ p := /-(λx, a1 = x)-/ - by cases p; cases q; exact idpo + 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)-/ - by cases p; rewrite [▸*,idp_con]; exact idpo + 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)-/ - by cases p; cases q; exact idpo + 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)-/ - by cases p; exact idpo + 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) := /-(λx, f x = g x)-/ - by cases p; rewrite [▸*,idp_con]; exact idpo + 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) : q =[p] (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := /-(λx, f x = g x)-/ - by cases p; rewrite [▸*,idp_con,ap_id];exact idpo + 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 := /-(λx, h (f x) = x)-/ - by cases p; rewrite [▸*,idp_con];exact idpo + 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)) := /-(λx, x = h (f x))-/ - by cases p; rewrite [▸*,idp_con];exact idpo + by induction p; rewrite [▸*,idp_con];exact idpo definition pathover_eq_r_idp (p : a1 = a2) : idp =[p] p := /-(λx, a1 = x)-/ - by cases p; exact idpo + by induction p; exact idpo definition pathover_eq_l_idp (p : a1 = a2) : idp =[p] p⁻¹ := /-(λx, x = a1)-/ - by cases p; exact idpo + by induction p; exact idpo definition pathover_eq_l_idp' (p : a1 = a2) : idp =[p⁻¹] p := /-(λx, x = a2)-/ - by cases p; exact idpo + by induction p; exact idpo -- The Functorial action of paths is [ap]. @@ -191,7 +207,7 @@ namespace eq is_equiv.mk (concat p) (concat p⁻¹) (con_inv_cancel_left p) (inv_con_cancel_left p) - (λq, by cases p;cases q;reflexivity) + (λ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) := @@ -202,7 +218,7 @@ namespace eq 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 cases p;cases q;reflexivity) + (λ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) := @@ -222,10 +238,10 @@ namespace eq apply concat2, {apply concat, {apply whisker_left_con_right}, apply concat2, - {cases p, cases q, reflexivity}, + {induction p, induction q, reflexivity}, {reflexivity}}, - {cases p, cases r, reflexivity}}, - {intro s, cases s, cases q, cases p, reflexivity} + {induction p, induction r, reflexivity}}, + {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) := @@ -236,8 +252,8 @@ namespace eq begin fapply adjointify, {intro s, apply (!cancel_right s)}, - {intro s, cases r, cases s, cases q, reflexivity}, - {intro s, cases s, cases r, cases p, reflexivity} + {intro s, induction r, cases s, induction q, reflexivity}, + {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) := @@ -253,9 +269,9 @@ namespace eq begin fapply adjointify, { apply eq_inv_con_of_con_eq}, - { intro s, cases r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq], + { intro s, induction r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq], con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]}, - { intro s, cases r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq], + { intro s, induction r, rewrite [↑[con_eq_of_eq_inv_con,eq_inv_con_of_con_eq], con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end @@ -268,10 +284,8 @@ namespace eq begin fapply adjointify, { apply eq_con_inv_of_con_eq}, - { intro s, cases p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq], - con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]}, - { intro s, cases p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq], - con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, + { intro s, induction p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_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) @@ -283,9 +297,9 @@ namespace eq begin fapply adjointify, { apply eq_con_of_inv_con_eq}, - { intro s, cases r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq], + { intro s, induction r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq], con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]}, - { intro s, cases r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq], + { intro s, induction r, rewrite [↑[inv_con_eq_of_eq_con,eq_con_of_inv_con_eq], con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end @@ -298,10 +312,8 @@ namespace eq begin fapply adjointify, { apply eq_con_of_con_inv_eq}, - { intro s, cases p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_eq], - con.assoc,con.assoc,con.left_inv,▸*,-con.assoc,con.right_inv,▸* at *,idp_con s]}, - { intro s, cases p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_eq], - con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, + { intro s, induction p, rewrite [↑[con_inv_eq_of_eq_con,eq_con_of_con_inv_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) @@ -333,37 +345,37 @@ namespace eq definition pathover_eq_equiv_l (p : a1 = a2) (q : a1 = a3) (r : a2 = a3) : q =[p] r ≃ q = p ⬝ r := /-(λx, x = a3)-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + 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)-/ - by cases p; apply pathover_idp + by induction p; apply pathover_idp definition pathover_eq_equiv_lr (p : a1 = a2) (q : a1 = a1) (r : a2 = a2) : q =[p] r ≃ q ⬝ p = p ⬝ r := /-(λx, x = x)-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + 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) : q =[p] r ≃ q = ap f p ⬝ r := /-(λx, f x = b)-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + 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) : q =[p] r ≃ q ⬝ ap f p = r := /-(λx, b = f x)-/ - by cases p; apply pathover_idp + by induction p; apply pathover_idp definition pathover_eq_equiv_FlFr (p : a1 = a2) (q : f a1 = g a1) (r : f a2 = g a2) : q =[p] r ≃ q ⬝ ap g p = ap f p ⬝ r := /-(λx, f x = g x)-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + 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) : q =[p] r ≃ q ⬝ p = ap h (ap f p) ⬝ r := /-(λx, h (f x) = x)-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + 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)) : q =[p] r ≃ q ⬝ ap h (ap f p) = p ⬝ r := /-(λx, x = h (f x))-/ - by cases p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ + by induction p; exact !pathover_idp ⬝e !equiv_eq_closed_right !idp_con⁻¹ -- a lot of this library still needs to be ported from Coq HoTT diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 232256b79..cbbf7ad15 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -135,7 +135,7 @@ namespace pointed definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) := begin - constructor, intro a, reflexivity, + fconstructor, intro a, reflexivity, cases A, cases B, cases C, cases D, cases f with f pf, cases g with g pg, cases h with h ph, esimp at *, induction pf, induction pg, induction ph, reflexivity @@ -143,14 +143,14 @@ namespace pointed definition pid_comp (f : A →* B) : pid B ∘* f ~* f := begin - constructor, + fconstructor, { intro a, reflexivity}, { esimp, exact !idp_con ⬝ !ap_id⁻¹} end definition comp_pid (f : A →* B) : f ∘* pid A ~* f := begin - constructor, + fconstructor, { intro a, reflexivity}, { reflexivity} end @@ -159,7 +159,7 @@ namespace pointed begin fapply equiv.MK, { intro f a, cases f with f p, exact f (some a)}, - { intro f, constructor, + { intro f, fconstructor, intro a, cases a, exact pt, exact f a, reflexivity}, { intro f, reflexivity}, @@ -193,7 +193,7 @@ namespace pointed begin fapply equiv.MK, { intro f, cases f with f p, exact f tt}, - { intro b, constructor, + { intro b, fconstructor, intro u, cases u, exact pt, exact b, reflexivity}, { intro b, reflexivity}, @@ -209,7 +209,7 @@ namespace pointed { intros A B f, rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Ω A), ↑Iterated_loop_space, ↓Iterated_loop_space n (Ω B)], apply IH (Ω A), - { esimp, constructor, + { esimp, fconstructor, intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt, esimp, apply con.left_inv}} end @@ -220,14 +220,14 @@ namespace pointed begin induction B, induction C, induction g with g pg, induction f with f pf, esimp at *, induction pg, induction pf, - constructor, - { intro p, esimp, apply whisker_left, exact ap_compose f g p ⬝ ap (ap g) !idp_con⁻¹}, + fconstructor, + { intro p, esimp, apply whisker_left, exact ap_compose g f p ⬝ ap (ap g) !idp_con⁻¹}, { reflexivity} end protected definition phomotopy.refl [refl] (f : A →* B) : f ~* f := begin - constructor, + fconstructor, { intro a, exact idp}, { apply idp_con} end @@ -235,7 +235,7 @@ namespace pointed protected definition phomotopy.trans [trans] (p : f ~* g) (q : g ~* h) : f ~* h := begin - constructor, + fconstructor, { intro a, exact p a ⬝ q a}, { induction f, induction g, induction p with p p', induction q with q q', esimp at *, induction p', induction q', esimp, apply con.assoc} @@ -243,7 +243,7 @@ namespace pointed protected definition phomotopy.symm [symm] (p : f ~* g) : g ~* f := begin - constructor, + fconstructor, { intro a, exact (p a)⁻¹}, { induction f, induction p with p p', esimp at *, induction p', esimp, apply inv_con_cancel_left} @@ -261,7 +261,7 @@ namespace pointed definition pwhisker_left (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g := begin - constructor, + fconstructor, { intro a, exact ap h (p a)}, { induction A, induction B, induction C, induction f with f pf, induction g with g pg, induction h with h ph, @@ -270,7 +270,7 @@ namespace pointed definition pwhisker_right (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h := begin - constructor, + fconstructor, { intro a, exact p (h a)}, { induction A, induction B, induction C, induction f with f pf, induction g with g pg, induction h with h ph, diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 41b246922..a017bcb58 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -27,10 +27,10 @@ namespace sigma | eta3 ⟨u₁, u₂, u₃, u₄⟩ := idp definition dpair_eq_dpair (p : a = a') (q : b =[p] b') : ⟨a, b⟩ = ⟨a', b'⟩ := - by cases q; reflexivity + by induction q; reflexivity definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v := - by cases u; cases v; exact (dpair_eq_dpair p q) + by induction u; induction v; exact (dpair_eq_dpair p q) /- Projections of paths from a total space -/ @@ -40,13 +40,13 @@ namespace sigma postfix `..1`:(max+1) := eq_pr1 definition eq_pr2 (p : u = v) : u.2 =[p..1] v.2 := - by cases p; exact idpo + by induction p; exact idpo postfix `..2`:(max+1) := eq_pr2 - private definition dpair_sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) + definition dpair_sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩ := - by cases u; cases v; cases q; apply idp + by induction u; induction v;esimp at *;induction q;esimp definition sigma_eq_pr1 (p : u.1 = v.1) (q : u.2 =[p] v.2) : (sigma_eq p q)..1 = p := (dpair_sigma_eq p q)..1 @@ -56,11 +56,11 @@ namespace sigma (dpair_sigma_eq p q)..2 definition sigma_eq_eta (p : u = v) : sigma_eq (p..1) (p..2) = p := - by cases p; cases u; reflexivity + by induction p; induction u; reflexivity definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : u.2 =[p] v.2) : transport (λx, B' x.1) (sigma_eq p q) = transport B' p := - by cases u; cases v; cases q; reflexivity + by induction u; induction v; esimp at *;induction q; reflexivity /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/ @@ -100,18 +100,18 @@ namespace sigma definition dpair_eq_dpair_con (p1 : a = a' ) (q1 : b =[p1] b' ) (p2 : a' = a'') (q2 : b' =[p2] b'') : dpair_eq_dpair (p1 ⬝ p2) (q1 ⬝o q2) = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 := - by cases q1; cases q2; reflexivity + by induction q1; induction q2; reflexivity definition sigma_eq_con (p1 : u.1 = v.1) (q1 : u.2 =[p1] v.2) (p2 : v.1 = w.1) (q2 : v.2 =[p2] w.2) : sigma_eq (p1 ⬝ p2) (q1 ⬝o q2) = sigma_eq p1 q1 ⬝ sigma_eq p2 q2 := - by cases u; cases v; cases w; apply dpair_eq_dpair_con + by induction u; induction v; induction w; apply dpair_eq_dpair_con local attribute dpair_eq_dpair [reducible] definition dpair_eq_dpair_con_idp (p : a = a') (q : b =[p] b') : dpair_eq_dpair p q = dpair_eq_dpair p !pathover_tr ⬝ dpair_eq_dpair idp (pathover_idp_of_eq (tr_eq_of_pathover q)) := - by cases q; reflexivity + by induction q; reflexivity /- eq_pr1 commutes with the groupoid structure. -/ @@ -123,24 +123,24 @@ namespace sigma definition ap_dpair (q : b₁ = b₂) : ap (sigma.mk a) q = dpair_eq_dpair idp (pathover_idp_of_eq q) := - by cases q; reflexivity + by induction q; reflexivity /- Dependent transport is the same as transport along a sigma_eq. -/ definition transportD_eq_transport (p : a = a') (c : C a b) : p ▸D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p !pathover_tr) c := - by cases p; reflexivity + by induction p; reflexivity definition sigma_eq_eq_sigma_eq {p1 q1 : a = a'} {p2 : b =[p1] b'} {q2 : b =[q1] b'} (r : p1 = q1) (s : p2 =[r] q2) : sigma_eq p1 p2 = sigma_eq q1 q2 := - by cases s; reflexivity + by induction s; reflexivity /- A path between paths in a total space is commonly shown component wise. -/ definition sigma_eq2 {p q : u = v} (r : p..1 = q..1) (s : p..2 =[r] q..2) : p = q := begin revert q r s, - cases p, cases u with u1 u2, + induction p, induction u with u1 u2, intro q r s, transitivity sigma_eq q..1 q..2, apply sigma_eq_eq_sigma_eq r s, @@ -158,30 +158,33 @@ namespace sigma definition transport_eq (p : a = a') (bc : Σ(b : B a), C a b) : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ := - by cases p; cases bc; reflexivity + by induction p; induction bc; reflexivity /- The special case when the second variable doesn't depend on the first is simpler. -/ definition tr_eq_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b) : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ := - by cases p; cases bc; reflexivity + by induction p; induction bc; reflexivity /- Or if the second variable contains a first component that doesn't depend on the first. -/ definition tr_eq2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a') (bcd : Σ(b : B a) (c : C a), D a b c) : p ▸ bcd = ⟨p ▸ bcd.1, p ▸ bcd.2.1, p ▸D2 bcd.2.2⟩ := begin - cases p, cases bcd with b cd, cases cd, reflexivity + induction p, induction bcd with b cd, induction cd, reflexivity end /- Pathovers -/ definition eta_pathover (p : a = a') (bc : Σ(b : B a), C a b) : bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ := - by cases p; cases bc; apply idpo + by induction p; induction bc; apply idpo definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b) (r : u.1 =[p] v.1) (s : u.2 =[apo011 C p r] v.2) : u =[p] v := - begin cases u, cases v, cases r, esimp [apo011] at s, induction s using idp_rec_on, apply idpo end + begin + induction u, induction v, esimp at *, induction r, + esimp [apo011] at s, induction s using idp_rec_on, apply idpo + end /- TODO: * define the projections from the type u =[p] v @@ -201,14 +204,14 @@ namespace sigma (sigma_functor f⁻¹ (λ(a' : A') (b' : B' a'), ((g (f⁻¹ a'))⁻¹ (transport B' (right_inv f a')⁻¹ b')))) begin - intro u', cases u' with a' b', + intro u', induction u' with a' b', apply sigma_eq (right_inv f a'), rewrite [▸*,right_inv (g (f⁻¹ a')),▸*], apply tr_pathover end begin intro u, - cases u with a b, + induction u with a b, apply (sigma_eq (left_inv f a)), apply pathover_of_tr_eq, rewrite [▸*,adj f,-(fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)), @@ -228,13 +231,13 @@ namespace sigma definition ap_sigma_functor_eq_dpair (p : a = a') (q : b =[p] b') : ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) := - by cases q; reflexivity + by induction q; reflexivity -- definition ap_sigma_functor_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) -- : ap (sigma_functor f g) (sigma_eq p q) = -- sigma_eq (ap f p) -- ((transport_compose B' f p (g u.1 u.2))⁻¹ ⬝ (fn_tr_eq_tr_fn p g u.2)⁻¹ ⬝ ap (g v.1) q) := - -- by cases u; cases v; apply ap_sigma_functor_eq_dpair + -- by induction u; induction v; apply ap_sigma_functor_eq_dpair /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/ open is_trunc @@ -265,8 +268,8 @@ namespace sigma equiv.mk _ (adjointify (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩) (λuc, ⟨uc.1.1, uc.1.2, !sigma.eta⁻¹ ▸ uc.2⟩) - begin intro uc, cases uc with u c, cases u, reflexivity end - begin intro av, cases av with a v, cases v, reflexivity end) + begin intro uc, induction uc with u c, induction u, reflexivity end + begin intro av, induction av with a v, induction v, reflexivity end) open prod prod.ops definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) := diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el index 19c612f09..3f80a5055 100644 --- a/src/emacs/lean-input.el +++ b/src/emacs/lean-input.el @@ -332,6 +332,7 @@ order for the change to take effect." ("transport" . ("▹")) ("con" . ("⬝")) ("cdot" . ("⬝")) + ("dot" . ("⬝")) ("sy" . ("⁻¹")) ("inv" . ("⁻¹")) ("-1" . ("⁻¹")) @@ -339,8 +340,12 @@ order for the change to take effect." ("-1e" . ("⁻¹ᵉ")) ("-1f" . ("⁻¹ᶠ")) ("-1h" . ("⁻¹ʰ")) + ("-1v" . ("⁻¹ᵛ")) + ("-1m" . ("⁻¹ᵐ")) ("-1g" . ("⁻¹ᵍ")) ("-1o" . ("⁻¹ᵒ")) + ("-2" . ("⁻²")) + ("-3" . ("⁻³")) ("qed" . ("∎")) ("x" . ("×")) ("o" . ("∘")) @@ -471,7 +476,7 @@ order for the change to take effect." ;; Squares. - ("sq" . ,(lean-input-to-string-list "■□◼◻◾◽▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳")) + ("sq" . ,(lean-input-to-string-list "◾◽■□◼◻▣▢▤▥▦▧▨▩◧◨◩◪◫◰◱◲◳")) ("sqb" . ,(lean-input-to-string-list "■◼◾")) ("sqw" . ,(lean-input-to-string-list "□◻◽")) ("sq." . ("▣")) diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 943c95a32..c19115905 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -141,7 +141,7 @@ "xrewrite" "krewrite" "esimp" "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "fconstructor" "left" "right" "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using" - "substvars")) + "substvars" "now")) word-end) (1 'font-lock-constant-face)) ;; Types