feat(hott): define pathovers and squares

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

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

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

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:
 

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 :=
+  definition to_inv [reducible] (f : A ≃ B) : B → A := f⁻¹
-  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

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 idp [reducible] {a : A} := refl a
-  definition idpath (a : A) := refl a
+  definition idpath [reducible] (a : A) := refl a
 
   -- unbased path induction
   definition rec' [reducible] {P : Π (a b : A), (a = b) -> Type}

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