From 5349839fa9f5b8eedb119d1bd1c7b0bfa774b758 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 10 Apr 2015 18:15:47 -0400 Subject: [PATCH] feat(hott): define pathovers and squares --- hott/cubical/cubical.md | 9 ++ hott/cubical/pathover.hlean | 270 ++++++++++++++++++++++++++++++++++++ hott/cubical/square.hlean | 128 +++++++++++++++++ hott/hott.md | 2 +- hott/init/equiv.hlean | 5 +- hott/init/path.hlean | 4 +- hott/types/eq.hlean | 4 +- 7 files changed, 415 insertions(+), 7 deletions(-) create mode 100644 hott/cubical/cubical.md create mode 100644 hott/cubical/pathover.hlean create mode 100644 hott/cubical/square.hlean diff --git a/hott/cubical/cubical.md b/hott/cubical/cubical.md new file mode 100644 index 000000000..d708d3c95 --- /dev/null +++ b/hott/cubical/cubical.md @@ -0,0 +1,9 @@ +hott.cubical +============ + +Implementation of Dan Licata's paper about [cubical ideas in HoTT](http://homotopytypetheory.org/2015/01/20/ts1s1-cubically/) + +* [pathover](pathover.hlean) +* [square](square.hlean) + +TODO: squareover/cube/cubeover \ No newline at end of file diff --git a/hott/cubical/pathover.hlean b/hott/cubical/pathover.hlean new file mode 100644 index 000000000..a561d75c6 --- /dev/null +++ b/hott/cubical/pathover.hlean @@ -0,0 +1,270 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: types.pathover +Author: Floris van Doorn + +Theorems about pathovers +-/ + +import .sigma arity + +open eq equiv is_equiv equiv.ops + +namespace cubical + + 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₄} + {b : B a} {b₂ : B a₂} {b₃ : B a₃} {b₄ : B a₄} + {c : C a b} {c₂ : C a₂ b₂} + {u v w : Σa, B a} + + inductive pathover (B : A → Type) (b : B a) : Π{a₂ : A} (p : a = a₂) (b₂ : B a₂), Type := + idpatho : pathover B b (refl a) b + + notation b `=[`:50 p:0 `]`:0 b₂:50 := pathover _ b p b₂ + + definition idpo [reducible] {b : B a} : b =[refl a] b := + pathover.idpatho b + + /- equivalences with equality using transport -/ + definition pathover_of_transport_eq (r : p ▹ b = b₂) : b =[p] b₂ := + by cases p; cases r; exact idpo + + definition pathover_of_eq_transport (r : b = p⁻¹ ▹ b₂) : b =[p] b₂ := + by cases p; cases r; exact idpo + + definition transport_eq_of_pathover (r : b =[p] b₂) : p ▹ b = b₂ := + by cases r; exact idp + + definition eq_transport_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▹ b₂ := + by cases r; exact idp + + definition pathover_equiv_transport_eq (p : a = a₂) (b : B a) (b₂ : B a₂) + : (b =[p] b₂) ≃ (p ▹ b = b₂) := + begin + fapply equiv.MK, + { exact transport_eq_of_pathover}, + { exact pathover_of_transport_eq}, + { intro r, cases p, cases r, apply idp}, + { intro r, cases r, apply idp}, + end + + definition pathover_equiv_eq_transport (p : a = a₂) (b : B a) (b₂ : B a₂) + : (b =[p] b₂) ≃ (b = p⁻¹ ▹ b₂) := + begin + fapply equiv.MK, + { exact eq_transport_of_pathover}, + { exact pathover_of_eq_transport}, + { intro r, cases p, cases r, apply idp}, + { intro r, cases r, apply idp}, + end + + definition pathover_transport (p : a = a₂) (b : B a) : b =[p] p ▹ b := + pathover_of_transport_eq idp + + definition transport_pathover (p : a = a₂) (b : B a) : p⁻¹ ▹ b =[p] b := + pathover_of_eq_transport 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 inverseo (r : b =[p] b₂) : b₂ =[p⁻¹] b := + pathover.rec_on r idpo + + definition apdo (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := + eq.rec_on p idpo + + infix `⬝o`:75 := concato + postfix `⁻¹ᵒ`:(max+10) := inverseo + + /- Some of the theorems analogous to theorems for = in init.path -/ + + definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo =[con_idp p] r := + pathover.rec_on r idpo + + definition idpo_cono (r : b =[p] b₂) : idpo ⬝o r =[idp_con p] r := + pathover.rec_on r idpo + + definition cono.assoc' (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) : + 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)) + + definition cono.assoc (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) : + (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 -/ + --set_option pp.notation false + definition pathover_constant (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' := + begin + fapply equiv.MK, + { intro r, cases r, exact idp}, + { intro r, cases p, cases r, exact idpo}, + { intro r, cases p, cases r, exact idp}, + { intro r, cases r, exact idp}, + end + + definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := + pathover_equiv_transport_eq idp b b' + + definition eq_of_pathover_idp {b' : B a} (q : b =[idpath a] b') : b = b' := + transport_eq_of_pathover q + + definition pathover_idp_of_eq {b' : B a} (q : b = b') : b =[idpath a] b' := + pathover_of_transport_eq q + + definition idp_rec_on {P : Π⦃b₂ : B a⦄, b =[idpath a] b₂ → Type} + {b₂ : B a} (r : b =[idpath a] b₂) (H : P idpo) : P r := + have H2 : P (pathover_idp_of_eq (eq_of_pathover_idp r)), + from eq.rec_on (eq_of_pathover_idp r) H, + left_inv !pathover_idp r ▹ H2 + + --pathover with fibration B' ∘ f + definition pathover_compose (B' : A' → Type) (f : A → A') (p : a = a₂) + (b : B' (f a)) (b₂ : B' (f a₂)) : b =[p] b₂ ≃ b =[ap f p] b₂ := + begin + fapply equiv.MK, + { intro r, cases r, exact idpo}, + { intro r, cases p, apply (idp_rec_on r), apply idpo}, + { intro r, cases p, esimp [function.compose,function.id], apply (idp_rec_on r), apply idp}, + { intro r, cases r, exact idp}, + end + + definition apdo_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃) + : apdo f (p ⬝ q) = apdo f p ⬝o apdo f q := + by cases p; cases q; exact idp + + open sigma sigma.ops + namespace sigma + /- pathovers used for sigma types -/ + definition dpair_eq_dpair (p : a = a₂) (q : b =[p] b₂) : ⟨a, b⟩ = ⟨a₂, b₂⟩ := + by cases q; apply idp + + definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v := + by cases u; cases v; apply (dpair_eq_dpair p q) + + /- Projections of paths from a total space -/ + + definition pathover_pr2 (p : u = v) : u.2 =[p..1] v.2 := + by cases p; apply idpo + + postfix `..2o`:(max+1) := pathover_pr2 + --superfluous notation, but useful if you want an 'o' on both projections + postfix [parsing-only] `..1o`:(max+1) := eq_pr1 + + private definition dpair_sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) + : ⟨(sigma_eq p q)..1, (sigma_eq p q)..2o⟩ = ⟨p, q⟩ := + by cases u; cases v; cases q; apply idp + + 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 + + definition sigma_eq_pr2 (p : u.1 = v.1) (q : u.2 =[p] v.2) + : (sigma_eq p q)..2o =[sigma_eq_pr1 p q] q := + (dpair_sigma_eq p q)..2o + + definition sigma_eq_eta (p : u = v) : sigma_eq (p..1) (p..2o) = p := + by cases p; cases u; apply idp + + /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/ + + definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v + | sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂ + + definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), + ⟨(sigma_eq_uncurried pq)..1, (sigma_eq_uncurried pq)..2o⟩ = pq + | dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂ + + definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2) + : (sigma_eq_uncurried pq)..1 = pq.1 := + (dpair_sigma_eq_uncurried pq)..1 + + definition sigma_eq_pr2_uncurried (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2) + : (sigma_eq_uncurried pq)..2o =[sigma_eq_pr1_uncurried pq] pq.2 := + (dpair_sigma_eq_uncurried pq)..2o + + definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried (sigma.mk p..1 p..2o) = p := + sigma_eq_eta p + + definition is_equiv_sigma_eq [instance] (u v : Σa, B a) + : is_equiv (@sigma_eq_uncurried A B u v) := + adjointify sigma_eq_uncurried + (λp, ⟨p..1, p..2o⟩) + sigma_eq_eta_uncurried + dpair_sigma_eq_uncurried + + definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1), u.2 =[p] v.2) ≃ (u = v) := + equiv.mk sigma_eq_uncurried !is_equiv_sigma_eq + + end sigma + + definition apD011o (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) + : f a b = f a₂ b₂ := + by cases Hb; exact idp + + definition apD0111o (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) + (Hc : c =[apD011o C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ := + by cases Hb; apply (idp_rec_on Hc); apply idp + + namespace pi + --the most 'natural' version here needs a notion of "path over a pathover" + definition pi_pathover {f : Πb, C a b} {g : Πb₂, C a₂ b₂} + (r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apD011o C p q] g b₂) : f =[p] g := + begin + cases p, apply pathover_idp_of_eq, + apply eq_of_homotopy, intro b, + apply eq_of_pathover_idp, apply r + end + + definition pi_pathover' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb₂, C ⟨a₂, b₂⟩} + (r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[sigma.dpair_eq_dpair p q] g b₂) + : f =[p] g := + begin + cases p, apply pathover_idp_of_eq, + apply eq_of_homotopy, intro b, + apply (@eq_of_pathover_idp _ C), exact (r b b (pathover.idpatho b)), + end + + definition ap11o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apD011o C p q] g b₂ := + by cases r; apply (idp_rec_on q); exact idpo + + definition ap10o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + {b : B a} : f b =[apD011o C p !pathover_transport] g (p ▹ b) := + by cases r; exact idpo + + -- definition equiv_pi_pathover' (f : Πb, C a b) (g : Πb₂, C a₂ b₂) : + -- (f =[p] g) ≃ (Π(b : B a), f b =[apD011o C p !pathover_transport] g (p ▹ b)) := + -- begin + -- fapply equiv.MK, + -- { exact ap10o}, + -- { exact pi_pathover'}, + -- { cases p, exact sorry}, + -- { intro r, cases r, }, + -- end + + + -- definition equiv_pi_pathover (f : Πb, C a b) (g : Πb₂, C a₂ b₂) : + -- (f =[p] g) ≃ (Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apD011o C p q] g b₂) := + -- begin + -- fapply equiv.MK, + -- { exact ap11o}, + -- { exact pi_pathover}, + -- { cases p, exact sorry}, + -- { intro r, cases r, }, + -- end + + end pi + + +end cubical diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean new file mode 100644 index 000000000..6639685de --- /dev/null +++ b/hott/cubical/square.hlean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: types.square +Author: Floris van Doorn + +Theorems about square +-/ + +import .sigma arity + +open eq equiv is_equiv + +namespace cubical + + variables {A : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A} + /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ + {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} + /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ + {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} + /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ + + + inductive square {A : Type} {a₀₀ : A} + : Π{a₂₀ a₀₂ a₂₂ : A}, a₀₀ = a₂₀ → a₀₂ = a₂₂ → a₀₀ = a₀₂ → a₂₀ = a₂₂ → Type := + ids : square idp idp idp idp + /- square top bottom left right -/ + + variables {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁} + {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃} + + definition ids [reducible] := @square.ids + definition idsquare [reducible] (a : A) := @square.ids A a + + definition hrefl (p : a = a') : square idp idp p p := + by cases p; exact ids + + definition vrefl (p : a = a') : square p p idp idp := + by cases p; exact ids + + definition hconcat (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) + : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ := + by cases s₃₁; exact s₁₁ + + definition vconcat (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃) + : square p₁₀ p₁₄ (p₀₁ ⬝ p₀₃) (p₂₁ ⬝ p₂₃) := + by cases s₁₃; exact s₁₁ + + definition hinverse (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₁₂⁻¹ p₂₁ p₀₁ := + by cases s₁₁;exact ids + + definition vinverse (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₂ p₁₀ p₀₁⁻¹ p₂₁⁻¹ := + by cases s₁₁;exact ids + + definition transpose (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := + by cases s₁₁;exact ids + + definition eq_of_square (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂ := + by cases s₁₁; apply idp + + definition hdegen_square {p q : a = a'} (r : p = q) : square idp idp p q := + by cases r;apply hrefl + + definition vdegen_square {p q : a = a'} (r : p = q) : square p q idp idp := + by cases r;apply vrefl + + 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 square_equiv_eq (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}, + end + + definition rec_on_b {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), + left_inv (to_fun !square_equiv_eq) s ▹ H2 + + definition rec_on_r {a₀₀ : A} + {P : Π{a₀₂ a₂₁ : A} {t : a₀₀ = a₂₁} {b : a₀₂ = a₂₁} {l : a₀₀ = a₀₂}, square t b l idp → Type} + {a₀₂ a₂₁ : A} {t : a₀₀ = a₂₁} {b : a₀₂ = a₂₁} {l : a₀₀ = a₀₂} + (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), + left_inv (to_fun !square_equiv_eq) s ▹ !inv_inv ▹ H2 + + definition rec_on_l {a₀₁ : A} + {P : Π {a₂₀ a₂₂ : A} {t : a₀₁ = a₂₀} {b : a₀₁ = a₂₂} {r : a₂₀ = a₂₂}, + square t b idp r → Type} + {a₂₀ a₂₂ : A} {t : a₀₁ = a₂₀} {b : a₀₁ = a₂₂} {r : a₂₀ = a₂₂} + (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), + left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2 + + definition rec_on_t {a₁₀ : A} + {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type} + {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂} + (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), + by rewrite [con_inv_cancel_right at H2, inv_inv at H2]; + exact (left_inv (to_fun !square_equiv_eq) s ▹ H2) + + definition rec_on_tb {a : A} + {P : Π{b : A} {l : a = b} {r : a = b}, square idp idp l r → Type} + {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), + left_inv (to_fun !square_equiv_eq) s ▹ H2 + + --we can also do the other recursors (lr, tl, tr, bl, br, tbl, tbr, tlr, blr), but let's postpone this until they are needed + +end cubical diff --git a/hott/hott.md b/hott/hott.md index 6fa314b9c..ec0780893 100644 --- a/hott/hott.md +++ b/hott/hott.md @@ -8,7 +8,7 @@ modules and directories: * [types](types/types.md) : concrete datatypes and type constructors * [hit](hit/hit.md): higher inductive types * [algebra](algebra/algebra.md) : algebraic structures - +* [cubical](cubical/cubical.md) : implementation of ideas from cubical type theory Lean's homotopy type theory kernel is a version of Martin-Löf Type Theory with: diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index c113a7f0f..709051d12 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -237,8 +237,9 @@ namespace equiv (right_inv : f ∘ g ∼ id) (left_inv : g ∘ f ∼ id) : A ≃ B := equiv.mk f (adjointify f g right_inv left_inv) - definition to_inv [reducible] (f : A ≃ B) : B → A := - f⁻¹ + definition to_inv [reducible] (f : A ≃ B) : B → A := f⁻¹ + definition to_right_inv [reducible] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f + definition to_left_inv [reducible] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f protected definition refl : A ≃ A := equiv.mk id !is_equiv_id diff --git a/hott/init/path.hlean b/hott/init/path.hlean index a656e2f51..b11a43d83 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -20,8 +20,8 @@ namespace eq --notation a = b := eq a b notation x = y `:>`:50 A:49 := @eq A x y - definition idp {a : A} := refl a - definition idpath (a : A) := refl a + definition idp [reducible] {a : A} := refl a + definition idpath [reducible] (a : A) := refl a -- unbased path induction definition rec' [reducible] {P : Π (a b : A), (a = b) -> Type} diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 0ea744240..8ebc04aed 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -148,7 +148,7 @@ namespace eq is_equiv.mk (concat p) (concat p⁻¹) (con_inv_cancel_left p) (inv_con_cancel_left p) - (eq.rec_on p (λq, eq.rec_on q idp)) + (λq, by cases p;cases q;exact idp) local attribute is_equiv_concat_left [instance] definition equiv_eq_closed_left (p : a1 = a2) (a3 : A) : (a1 = a3) ≃ (a2 = a3) := @@ -159,7 +159,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) - (eq.rec_on p (λq, eq.rec_on q idp)) + (λq, by cases p;cases q;exact idp) local attribute is_equiv_concat_right [instance] definition equiv_eq_closed_right (p : a2 = a3) (a1 : A) : (a1 = a2) ≃ (a1 = a3) :=