michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): various clean-up and small additions

Browse source
This commit is contained in:
Floris van Doorn 2015-06-23 12:47:52 -04:00
parent 2748525c21
commit ea0f57aef5
18 changed files with 532 additions and 341 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
hott/arity.hlean
View file

@ -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

18
hott/hit/sphere.hlean
View file

@ -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

22
hott/hit/susp.hlean
View file

@ -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

12
hott/init/equiv.hlean
View file

@ -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 _

17
hott/init/funext.hlean
View file

@ -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

2
hott/init/hit.hlean
View file

@ -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}

84
hott/init/path.hlean
View file

@ -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

84
hott/init/pathover.hlean
View file

@ -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

8
hott/types/cubical/cubical.md
View file

@ -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)
* [cubeover](cubeover.hlean): cube over a cube

1
hott/types/cubical/default.hlean
View file

@ -5,4 +5,3 @@ Authors: Floris van Doorn
-/
import .square .cube .squareover .cubeover
import .pathover

50
hott/types/cubical/pathover.hlean
View file

@ -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

273
hott/types/cubical/square.hlean
View file

@ -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

66
hott/types/cubical/squareover.hlean
View file

@ -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

128
hott/types/eq.hlean
View file

@ -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

26
hott/types/pointed.hlean
View file

@ -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,

53
hott/types/sigma.hlean
View file

@ -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) :=

7
src/emacs/lean-input.el
View file

@ -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." . ("▣"))

2
src/emacs/lean-syntax.el
View file

@ -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