feat(hott): use pathovers in all the recursors of hits

move pathover file to the init folder

hott/algebra/category/constructions/comma.hlean

@@ -1,14 +1,15 @@
 /-
 Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Jakob von Raumer
+
+Authors: Floris van Doorn
 
 Comma category
 -/
 
-import ..functor cubical.pathover ..strict ..category
+import ..functor ..strict ..category
 
-open eq functor equiv sigma sigma.ops is_trunc cubical iso is_equiv
+open eq functor equiv sigma sigma.ops is_trunc iso is_equiv
 
 namespace category
 

hott/algebra/hott.hlean

@@ -6,9 +6,9 @@ Author: Floris van Doorn
 Theorems about algebra specific to HoTT
 -/
 
-import .group arity types.pi types.hprop_trunc cubical.pathover
+import .group arity types.pi types.hprop_trunc
 
-open equiv eq equiv.ops is_trunc cubical
+open equiv eq equiv.ops is_trunc
 
 namespace algebra
   open Group has_mul has_inv
@@ -55,7 +55,7 @@ namespace algebra
     (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
   begin
     cases G with Gc G, cases H with Hc H,
-    apply (apd011o mk (ua f)),
+    apply (apo011 mk (ua f)),
     apply group_pathover, exact resp_mul
   end
 

hott/core.hlean

@@ -7,5 +7,6 @@ The core of the HoTT library
 -/
 
 import types
-import cubical.pathover cubical.square
+import cubical.square
 import hit.circle
+import algebra.hott

hott/cubical/pathover.hlean

@@ -1,268 +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
-
-Theorems about pathovers
--/
-
-import types.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] [constructor] {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 [recursor] {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/hit/circle.hlean

@@ -20,10 +20,10 @@ namespace circle
   definition seg2 : base1 = base2 := merid !south
 
   definition base : circle := base1
-  definition loop : base = base := seg1 ⬝ seg2⁻¹
+  definition loop : base = base := seg2 ⬝ seg1⁻¹
 
   definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) (x : circle) : P x :=
+    (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) (x : circle) : P x :=
   begin
     induction x with b,
     { exact Pb1},
@@ -35,21 +35,21 @@ namespace circle
   end
 
   definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) : P x :=
+    (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) : P x :=
   circle.rec2 Pb1 Pb2 Ps1 Ps2 x
 
   theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2)
+    (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2)
-      : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
+      : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   !rec_merid
 
   theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2)
+    (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2)
-      : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
+      : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   !rec_merid
 
   definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 Ps2 : Pb1 = Pb2) (x : circle) : P :=
-  rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x
+  rec2 Pb1 Pb2 (pathover_of_eq Ps1) (pathover_of_eq Ps2) x
 
   definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P)
     (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : P :=
@@ -58,15 +58,15 @@ namespace circle
   theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant seg1 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant seg1),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg1],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg1],
   end
 
   theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant seg2),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg2],
   end
 
   definition elim2_type (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2) (x : circle) : Type :=
@@ -84,41 +84,38 @@ namespace circle
     : transport (elim2_type Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   by rewrite [tr_eq_cast_ap_fn,↑elim2_type,elim2_seg2];apply cast_ua_fn
 
-  protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase)
+  protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase)
     (x : circle) : P x :=
   begin
     fapply (rec2_on x),
     { exact Pbase},
     { exact (transport P seg1 Pbase)},
-    { apply idp},
+    { apply pathover_tr},
-    { apply tr_eq_of_eq_inv_tr, exact (Ploop⁻¹ ⬝ !con_tr)},
+    { apply pathover_tr_of_pathover, exact Ploop}
   end
---rewrite -tr_con, exact Ploop⁻¹
 
   protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
-    (Ploop : loop ▸ Pbase = Pbase) : P x :=
+    (Ploop : Pbase =[loop] Pbase) : P x :=
   circle.rec Pbase Ploop x
 
   theorem rec_loop_helper {A : Type} (P : A → Type)
-    {x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▸ v) :
+    {x y z : A} {p : x = y} {p' : z = y} {u : P x} {v : P z} (q : u =[p ⬝ p'⁻¹] v) :
-    eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q :=
+    pathover_tr_of_pathover q ⬝o !pathover_tr⁻¹ᵒ = q :=
-  by cases p; exact idp
+  by cases p'; cases q; exact idp
 
   definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p :=
   eq.rec_on p idp
 
-  theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase) :
+  theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) :
-    apd (circle.rec Pbase Ploop) loop = Ploop :=
+    apdo (circle.rec Pbase Ploop) loop = Ploop :=
   begin
-    rewrite [↑loop,apd_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here
+    rewrite [↑loop,apdo_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apdo_inv,rec2_seg1],
-    apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp,
+    apply rec_loop_helper
-    rewrite [rec_loop_helper,inv_con_inv_left],
-    apply con_inv_cancel_left
   end
 
   protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
     (x : circle) : P :=
-  circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x
+  circle.rec Pbase (pathover_of_eq Ploop) x
 
   protected definition elim_on [reducible] {P : Type} (x : circle) (Pbase : P)
     (Ploop : Pbase = Pbase) : P :=
@@ -127,8 +124,8 @@ namespace circle
   theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
     ap (circle.elim Pbase Ploop) loop = Ploop :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant loop (circle.elim Pbase Ploop base))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant loop),
-    rewrite [-apd_eq_tr_constant_con_ap,↑circle.elim,rec_loop],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,rec_loop],
   end
 
   protected definition elim_type (Pbase : Type) (Ploop : Pbase ≃ Pbase)
@@ -149,7 +146,7 @@ namespace circle
 end circle
 
 attribute circle.base1 circle.base2 circle.base [constructor]
-attribute circle.rec2 circle.elim2 [unfold-c 6] [recursor 6]
+attribute circle.elim2 circle.rec2 [unfold-c 6] [recursor 6]
 attribute circle.elim2_type [unfold-c 5]
 attribute circle.rec2_on circle.elim2_on [unfold-c 2]
 attribute circle.elim2_type [unfold-c 1]
@@ -164,17 +161,22 @@ namespace circle
 
   definition loop_neq_idp : loop ≠ idp :=
   assume H : loop = idp,
-  have H2 : Π{A : Type₁} {a : A} (p : a = a), p = idp,
+  have H2 : Π{A : Type₁} {a : A} {p : a = a}, p = idp,
     from λA a p, calc
       p   = ap (circle.elim a p) loop : elim_loop
       ... = ap (circle.elim a p) (refl base) : by rewrite H,
-  absurd !H2 eq_bnot_ne_idp
+  absurd H2 eq_bnot_ne_idp
 
   definition nonidp (x : circle) : x = x :=
-  circle.rec_on x loop
+  begin
-    (calc
+    induction x,
-      loop ▸ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr
+    { exact loop},
-        ... = loop : by rewrite [con.left_inv, idp_con])
+    { exact sorry}
+  end
+  -- circle.rec_on x loop
+  --   (calc
+  --     loop ▸ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr
+  --       ... = loop : by rewrite [con.left_inv, idp_con])
 
   definition nonidp_neq_idp : nonidp ≠ (λx, idp) :=
   assume H : nonidp = λx, idp,
@@ -200,9 +202,10 @@ namespace circle
   begin
     induction x,
     { exact power loop},
-    { apply eq_of_homotopy, intro a,
+    { apply sorry}
-      refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
+-- apply eq_of_homotopy, intro a,
-      rewrite [transport_code_loop_inv,power_con,succ_pred]}
+--       refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
+--       rewrite [transport_code_loop_inv,power_con,succ_pred]}
   end
 
   --remove this theorem after #484
@@ -219,11 +222,11 @@ namespace circle
         apply transport (λ(y : base = base), transport circle.code y _ = _),
         { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
         rewrite [▸*,@con_tr _ circle.code,transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ]}},
-    { apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [circle.code,base,base1], exact _}
+    --{ apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [circle.code,base,base1], exact _}
+      { apply sorry}
         --simplify after #587
   end
 
-
   definition circle_eq_equiv (x : circle) : (base = x) ≃ circle.code x :=
   begin
     fapply equiv.MK,

hott/hit/coeq.hlean

@@ -31,7 +31,7 @@ parameters {A B : Type.{u}} (f g : A → B)
   eq_of_rel coeq_rel (Rmk f g x)
 
   protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
-    (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
+    (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) (y : coeq) : P y :=
   begin
     induction y,
     { apply P_i},
@@ -39,17 +39,17 @@ parameters {A B : Type.{u}} (f g : A → B)
   end
 
   protected definition rec_on [reducible] {P : coeq → Type} (y : coeq)
-    (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) : P y :=
+    (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) : P y :=
   rec P_i Pcp y
 
   theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
-    (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x))
+    (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x))
-      (x : A) : apd (rec P_i Pcp) (cp x) = Pcp x :=
+      (x : A) : apdo (rec P_i Pcp) (cp x) = Pcp x :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (P_i : B → P)
     (Pcp : Π(x : A), P_i (f x) = P_i (g x)) (y : coeq) : P :=
-  rec P_i (λx, !tr_constant ⬝ Pcp x) y
+  rec P_i (λx, pathover_of_eq (Pcp x)) y
 
   protected definition elim_on [reducible] {P : Type} (y : coeq) (P_i : B → P)
     (Pcp : Π(x : A), P_i (f x) = P_i (g x)) : P :=
@@ -58,8 +58,8 @@ parameters {A B : Type.{u}} (f g : A → B)
   theorem elim_cp {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x))
     (x : A) : ap (elim P_i Pcp) (cp x) = Pcp x :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (cp x) (elim P_i Pcp (coeq_i (f x))))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (cp x)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cp],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cp],
   end
 
   protected definition elim_type (P_i : B → Type)

hott/hit/colimit.hlean

@@ -34,7 +34,7 @@ section
 
    protected definition rec {P : colimit → Type}
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x)
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x)
       (y : colimit) : P y :=
   begin
     fapply (type_quotient.rec_on y),
@@ -44,18 +44,18 @@ section
 
   protected definition rec_on [reducible] {P : colimit → Type} (y : colimit)
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x) : P y :=
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) : P y :=
   rec Pincl Pglue y
 
   theorem rec_cglue {P : colimit → Type}
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x)
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x)
-      {j : J} (x : A (dom j)) : apd (rec Pincl Pglue) (cglue j x) = Pglue j x :=
+      {j : J} (x : A (dom j)) : apdo (rec Pincl Pglue) (cglue j x) = Pglue j x :=
   !rec_eq_of_rel
 
-   protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
+  protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
     (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P :=
-  rec Pincl (λj a, !tr_constant ⬝ Pglue j a) y
+  rec Pincl (λj a, pathover_of_eq (Pglue j a)) y
 
   protected definition elim_on [reducible] {P : Type} (y : colimit)
     (Pincl : Π⦃i : I⦄ (x : A i), P)
@@ -67,8 +67,8 @@ section
     (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x)
       {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (cglue j x) (elim Pincl Pglue (ι (f j x))))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cglue],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cglue],
   end
 
   protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type)
@@ -118,7 +118,7 @@ section
 
   protected definition rec {P : seq_colim → Type}
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π(n : ℕ) (a : A n), glue a ▸ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa :=
+    (Pglue : Π(n : ℕ) (a : A n), Pincl (f a) =[glue a] Pincl a) (aa : seq_colim) : P aa :=
   begin
     fapply (type_quotient.rec_on aa),
     { intro a, cases a, apply Pincl},
@@ -127,18 +127,18 @@ section
 
   protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim)
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a)
+    (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a)
       : P aa :=
   rec Pincl Pglue aa
 
   theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
+    (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) {n : ℕ} (a : A n)
-      : apd (rec Pincl Pglue) (glue a) = Pglue a :=
+      : apdo (rec Pincl Pglue) (glue a) = Pglue a :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
     (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P :=
-  rec Pincl (λn a, !tr_constant ⬝ Pglue a)
+  rec Pincl (λn a, pathover_of_eq (Pglue a))
 
   protected definition elim_on [reducible] {P : Type} (aa : seq_colim)
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
@@ -149,8 +149,8 @@ section
     (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
       : ap (elim Pincl Pglue) (glue a) = Pglue a :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (glue a) (elim Pincl Pglue (sι (f a))))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_glue],
   end
 
   protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)

hott/hit/cylinder.hlean

@@ -35,7 +35,7 @@ parameters {A B : Type.{u}} (f : A → B)
 
   protected definition rec {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
-    (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) (x : cylinder) : P x :=
+    (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a) (x : cylinder) : P x :=
   begin
     induction x,
     { cases a,
@@ -46,18 +46,18 @@ parameters {A B : Type.{u}} (f : A → B)
 
   protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder)
     (Pbase : Π(b : B), P (base b)) (Ptop  : Π(a : A), P (top a))
-    (Pseg  : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) : P x :=
+    (Pseg  : Π(a : A), Pbase (f a) =[seg a] Ptop a) : P x :=
   rec Pbase Ptop Pseg x
 
   theorem rec_seg {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
-    (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a)
+    (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a)
-      (a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
+      (a : A) : apdo (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
     (Pseg : Π(a : A), Pbase (f a) = Ptop a) (x : cylinder) : P :=
-  rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x
+  rec Pbase Ptop (λa, pathover_of_eq (Pseg a)) x
 
   protected definition elim_on [reducible] {P : Type} (x : cylinder) (Pbase : B → P) (Ptop : A → P)
     (Pseg : Π(a : A), Pbase (f a) = Ptop a) : P :=
@@ -67,8 +67,8 @@ parameters {A B : Type.{u}} (f : A → B)
     (Pseg : Π(a : A), Pbase (f a) = Ptop a)
     (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (seg a) (elim Pbase Ptop Pseg (base (f a))))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_seg],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_seg],
   end
 
   protected definition elim_type (Pbase : B → Type) (Ptop : A → Type)

hott/hit/pushout.hlean

@@ -33,7 +33,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
   eq_of_rel pushout_rel (Rmk f g x)
 
   protected definition rec {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
-    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
+    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x))
       (y : pushout) : P y :=
   begin
     induction y,
@@ -45,17 +45,17 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
 
   protected definition rec_on [reducible] {P : pushout → Type} (y : pushout)
     (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x))
-    (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x)) : P y :=
+    (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x)) : P y :=
   rec Pinl Pinr Pglue y
 
   theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
-    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x))
+    (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x))
-      (x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
+      (x : TL) : apdo (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
     (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P :=
-  rec Pinl Pinr (λx, !tr_constant ⬝ Pglue x) y
+  rec Pinl Pinr (λx, pathover_of_eq (Pglue x)) y
 
   protected definition elim_on [reducible] {P : Type} (y : pushout) (Pinl : BL → P)
     (Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) : P :=
@@ -65,8 +65,8 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
     (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (x : TL)
     : ap (elim Pinl Pinr Pglue) (glue x) = Pglue x :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (glue x) (elim Pinl Pinr Pglue (inl (f x))))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (glue x)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue],
   end
 
   protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type)

hott/hit/quotient.hlean

@@ -8,7 +8,7 @@ Declaration of set-quotients
 
 import .type_quotient .trunc
 
-open eq is_trunc trunc type_quotient
+open eq is_trunc trunc type_quotient equiv
 
 namespace quotient
 section
@@ -26,30 +26,29 @@ parameters {A : Type} (R : A → A → hprop)
   begin unfold quotient, exact _ end
 
   protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
-    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a')
     (x : quotient) : P x :=
   begin
     apply (@trunc.rec_on _ _ P x),
     { intro x', apply Pt},
     { intro y, fapply (type_quotient.rec_on y),
       { exact Pc},
-      { intros,
+      { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}}
-        apply concat, apply transport_compose; apply Pp}}
   end
 
   protected definition rec_on [reducible] {P : quotient → Type} (x : quotient)
     [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a))
-    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a') : P x :=
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') : P x :=
   rec Pc Pp x
 
   theorem rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
-    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a')
-    {a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H :=
+    {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H :=
-  !is_hset.elim
+  !is_hset.elimo
 
   protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P)
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P :=
-  rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
+  rec Pc (λa a' H, pathover_of_eq (Pp H)) x
 
   protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_hset P]
     (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')  : P :=
@@ -59,8 +58,8 @@ parameters {A : Type} (R : A → A → hprop)
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
     : ap (elim Pc Pp) (eq_of_rel H) = Pp H :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel H) (elim Pc Pp (class_of a)))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_eq_of_rel],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel],
   end
 
   /-

hott/hit/suspension.hlean

@@ -25,7 +25,7 @@ namespace suspension
   glue _ _ a
 
   protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), merid a ▸ PN = PS) (x : suspension A) : P x :=
+    (Pm : Π(a : A), PN =[merid a] PS) (x : suspension A) : P x :=
   begin
     fapply (pushout.rec_on _ _ x),
     { intro u, cases u, exact PN},
@@ -34,17 +34,17 @@ namespace suspension
   end
 
   protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A)
-    (PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▸ PN = PS) : P y :=
+    (PN : P !north) (PS : P !south) (Pm : Π(a : A), PN =[merid a] PS) : P y :=
   suspension.rec PN PS Pm y
 
   theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
-    (Pm : Π(a : A), merid a ▸ PN = PS) (a : A)
+    (Pm : Π(a : A), PN =[merid a] PS) (a : A)
-      : apd (suspension.rec PN PS Pm) (merid a) = Pm a :=
+      : apdo (suspension.rec PN PS Pm) (merid a) = Pm a :=
   !rec_glue
 
   protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
     (x : suspension A) : P :=
-  suspension.rec PN PS (λa, !tr_constant ⬝ Pm a) x
+  suspension.rec PN PS (λa, pathover_of_eq (Pm a)) x
 
   protected definition elim_on [reducible] {P : Type} (x : suspension A)
     (PN : P) (PS : P)  (Pm : A → PN = PS) : P :=
@@ -53,8 +53,8 @@ namespace suspension
   theorem elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (a : A)
     : ap (suspension.elim PN PS Pm) (merid a) = Pm a :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (merid a) (suspension.elim PN PS Pm !north))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑suspension.elim,rec_merid],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑suspension.elim,rec_merid],
   end
 
   protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)

hott/hit/type_quotient.hlean

@@ -16,7 +16,7 @@ namespace type_quotient
 
   protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')
     (x : type_quotient R) : P :=
-  type_quotient.rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
+  type_quotient.rec Pc (λa a' H, pathover_of_eq (Pp H)) x
 
   protected definition elim_on [reducible] {P : Type} (x : type_quotient R)
     (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
@@ -26,8 +26,8 @@ namespace type_quotient
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
     : ap (type_quotient.elim Pc Pp) (eq_of_rel R H) = Pp H :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel R H) (type_quotient.elim Pc Pp (class_of R a)))),
+    apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)),
-    rewrite [-apd_eq_tr_constant_con_ap,↑type_quotient.elim,rec_eq_of_rel],
+    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑type_quotient.elim,rec_eq_of_rel],
   end
 
   protected definition elim_type (Pc : A → Type)

hott/init/default.hlean

@@ -10,7 +10,7 @@ import init.bool init.num init.priority init.relation init.wf
 import init.types
 import init.trunc init.path init.equiv init.util
 import init.ua init.funext
-import init.hedberg init.nat init.hit
+import init.hedberg init.nat init.hit init.pathover
 
 namespace core
   export bool empty unit sum

hott/init/equiv.hlean

@@ -28,7 +28,6 @@ structure equiv (A B : Type) :=
   (to_fun : A → B)
   (to_is_equiv : is_equiv to_fun)
 
-
 namespace is_equiv
   /- Some instances and closure properties of equivalences -/
   postfix `⁻¹` := inv
@@ -157,9 +156,13 @@ namespace is_equiv
   have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
   @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a))
 
-  definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) :=
+  definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y :=
-    adjointify (ap f)
+  (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
-      (λq, (inverse (left_inv f x)) ⬝ ap f⁻¹ q ⬝ left_inv f y)
+
+  definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f : x = y → f x = f y) :=
+    adjointify
+      (ap f)
+      (eq_of_fn_eq_fn' f)
       (λq, !ap_con
         ⬝ whisker_right !ap_con _
         ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
@@ -252,7 +255,7 @@ namespace equiv
   protected definition refl [refl] [constructor] : A ≃ A :=
   equiv.mk id !is_equiv_id
 
-  protected definition symm [symm] (f : A ≃ B) : B ≃ A :=
+  protected definition symm [symm] [unfold-c 3] (f : A ≃ B) : B ≃ A :=
   equiv.mk f⁻¹ !is_equiv_inv
 
   protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
@@ -270,6 +273,12 @@ namespace equiv
   definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
   equiv.mk (transport P p) !is_equiv_tr
 
+  definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y :=
+  (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
+
+  definition eq_of_fn_eq_fn_inv (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y :=
+  (right_inv f x)⁻¹ ⬝ ap f q ⬝ right_inv f y
+
   --we need this theorem for the funext_of_ua proof
   theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
   eq.rec_on p idp
@@ -280,7 +289,10 @@ namespace equiv
   namespace ops
     infixl `⬝e`:75 := equiv.trans
     postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
-    postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded
+    postfix [parsing-only] `⁻¹ᵉ`:(max + 1) := equiv.symm
+      -- notation for inverse which is not overloaded
     abbreviation erfl [constructor] := @equiv.refl
   end ops
 end equiv
+
+export [unfold-hints] equiv [unfold-hints] is_equiv

hott/init/hit.hlean

@@ -8,7 +8,7 @@ Declaration of the primitive hits in Lean
 
 prelude
 
-import .trunc
+import .trunc .pathover
 
 open is_trunc eq
 
@@ -55,12 +55,12 @@ namespace type_quotient
     : class_of R a = class_of R a'
 
   protected constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a')
     (x : type_quotient R) : P x
 
   protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
     (x : type_quotient R) (Pc : Π(a : A), P (class_of R a))
-    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') : P x :=
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') : P x :=
   type_quotient.rec Pc Pp x
 
 end type_quotient
@@ -75,13 +75,13 @@ end trunc
 
 namespace type_quotient
   definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a')
     (a : A) : type_quotient.rec Pc Pp (class_of R a) = Pc a :=
   idp
 
   constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a')
-    {a a' : A} (H : R a a') : apd (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
+    {a a' : A} (H : R a a') : apdo (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
 end type_quotient
 
 attribute type_quotient.class_of trunc.tr [constructor]

hott/init/init.md

@@ -24,6 +24,7 @@ Datatypes and logic:
 HoTT basics:
 
 * [path](path.hlean)
+* [pathover](pathover.hlean) 
 * [hedberg](hedberg.hlean)
 * [trunc](trunc.hlean)
 * [equiv](equiv.hlean)

hott/init/pathover.hlean

@@ -0,0 +1,183 @@
+/-
+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
+
+Basic theorems about pathovers
+-/
+
+prelude
+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₄}
+          {b : B a} {b₂ : B a₂} {b₃ : B a₃} {b₄ : B a₄}
+          {c : C a b} {c₂ : C a₂ b₂}
+
+namespace eq
+  inductive pathover.{l} (B : A → Type.{l}) (b : B a) : Π{a₂ : A}, a = a₂ → B a₂ → Type.{l} :=
+  idpatho : pathover B b (refl a) b
+
+  notation b `=[`:50 p:0 `]`:0 b₂:50 := pathover _ b p b₂
+
+  definition idpo [reducible] [constructor] : b =[refl a] b :=
+  pathover.idpatho b
+
+  /- equivalences with equality using transport -/
+  definition pathover_of_tr_eq (r : p ▸ b = b₂) : b =[p] b₂ :=
+  by cases p; cases r; exact idpo
+
+  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₂ :=
+  by cases r; exact idp
+
+  definition eq_tr_of_pathover (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₂)
+    : (b =[p] b₂) ≃ (p ▸ b = b₂) :=
+  begin
+    fapply equiv.MK,
+    { exact tr_eq_of_pathover},
+    { exact pathover_of_tr_eq},
+    { intro r, cases p, cases r, apply idp},
+    { intro r, cases r, apply idp},
+  end
+
+  definition pathover_equiv_eq_tr (p : a = a₂) (b : B a) (b₂ : B a₂)
+    : (b =[p] b₂) ≃ (b = p⁻¹ ▸ b₂) :=
+  begin
+    fapply equiv.MK,
+    { exact eq_tr_of_pathover},
+    { exact pathover_of_eq_tr},
+    { intro r, cases p, cases r, apply idp},
+    { 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 tr_pathover (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 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 `⬝` := concato
+  infix `⬝o`:75 := concato
+  -- postfix `⁻¹` := inverseo
+  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 -/
+
+  definition eq_of_pathover {a' a₂' : A'} (q : a' =[p] a₂') : a' = a₂' :=
+  by cases q;reflexivity
+
+  definition pathover_of_eq {a' a₂' : A'} (q : a' = a₂') : a' =[p] a₂' :=
+  by cases p;cases q;exact idpo
+
+  definition pathover_constant [constructor] (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' :=
+  begin
+    fapply equiv.MK,
+    { exact eq_of_pathover},
+    { exact pathover_of_eq},
+    { 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_tr_eq idp b b'
+
+  definition eq_of_pathover_idp {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
+
+  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 :=
+  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
+
+  definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ :=
+  by cases p; exact idp
+
+  definition apdo_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) :
+    apdo f p = pathover_of_eq (ap f p) :=
+  eq.rec_on p idp
+
+  definition pathover_of_pathover_tr (q : b =[p ⬝ p₂] p₂ ▸ b₂) : b =[p] b₂ :=
+  by cases p₂;exact q
+
+  definition pathover_tr_of_pathover {p : a = a₃} (q : b =[p ⬝ p₂⁻¹] b₂) : b =[p] p₂ ▸ b₂ :=
+  by cases p₂;exact q
+
+  definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
+      : f a b = f a₂ b₂ :=
+  by cases Hb; exact idp
+
+  definition apo0111 (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
+    (Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
+  by cases Hb; apply (idp_rec_on Hc); apply idp
+
+  definition apo11 {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 =[apo011 C p q] g b₂ :=
+  by cases r; apply (idp_rec_on q); exact idpo
+
+  definition apo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
+    {b : B a} : f b =[apo011 C p !pathover_tr] g (p ▸ b) :=
+  by cases r; exact idpo
+
+
+end eq

hott/init/trunc.hlean

@@ -11,7 +11,7 @@ Ported from Coq HoTT.
 --TODO: can we replace some definitions with a hprop as codomain by theorems?
 
 prelude
-import .logic .equiv .types
+import .logic .equiv .types .pathover
 open eq nat sigma unit
 
 namespace is_trunc
@@ -270,6 +270,22 @@ namespace is_trunc
            (λ (u : unit), unit.rec_on u idp)
            (λ (x : A), center_eq x)
 
+  /- interaction with pathovers -/
+  variables {C : A → Type}
+            {a a₂ : A} (p : a = a₂)
+            (c : C a) (c₂ : C a₂)
+
+  definition is_hprop.elimo [H : is_hprop (C a)] : c =[p] c₂ :=
+  pathover_of_eq_tr !is_hprop.elim
+
+  definition is_trunc_pathover [instance]
+    (n : trunc_index) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) :=
+  is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr
+
+  variables {p c c₂}
+  theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' :=
+  !is_hprop.elim
+
   -- TODO: port "Truncated morphisms"
 
 end is_trunc

hott/types/int/default.hlean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .basic
+import .basic .hott