From 0ec525a8eed3ec1a0db0faad115d4c0bdd9ffd95 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 4 Aug 2015 19:00:12 +0200 Subject: [PATCH] feat(two_quotient): finish proof of elim_incl2 --- hott/algebra/e_closure.hlean | 2 +- hott/hit/torus.hlean | 11 +++---- hott/hit/two_quotient.hlean | 22 +++++++++---- hott/init/equiv.hlean | 22 ++++++++++--- hott/init/path.hlean | 6 ++-- hott/init/pathover.hlean | 4 +-- hott/types/cubical/cube.hlean | 2 +- hott/types/cubical/square.hlean | 6 +++- hott/types/cubical/squareover.hlean | 24 ++++++++++++-- hott/types/eq.hlean | 50 ++++++++++++++++++++++------- hott/types/eq2.hlean | 5 +++ hott/types/pi.hlean | 2 +- 12 files changed, 115 insertions(+), 41 deletions(-) diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 4218d46c5..9b7137c0a 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -33,7 +33,7 @@ section variables ⦃a a' : A⦄ {s : R a a'} {r : T a a} parameter {R} - protected definition e_closure.elim [unfold 6] {B : Type} {f : A → B} + protected definition e_closure.elim [unfold 8] {B : Type} {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' := begin induction t, diff --git a/hott/hit/torus.hlean b/hott/hit/torus.hlean index b7ffb43a3..266885572 100644 --- a/hott/hit/torus.hlean +++ b/hott/hit/torus.hlean @@ -76,16 +76,13 @@ namespace torus (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 := !elim_incl1 -/- - TODO(Leo): uncomment after we finish elim_incl2 definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) - : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf) - Ps - (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2)) - (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) := + : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf) + Ps + (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2)) + (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) := !elim_incl2 --/ end torus diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 11e84995c..a6072a28c 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -296,21 +296,29 @@ namespace two_quotient ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t := !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t -/- - --print elim theorem elim_incl2 {P : Type} (P0 : A → P) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t') ⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t') : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') := begin - -- let H := elim_incl2 R Q2 P0 P1 (two_quotient_Q.rec (λ (a a' : A) (t t' : T a a') (q : Q t t'), con_inv_eq_idp (P2 q))) (Qmk R q), - -- esimp at H, rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp], - xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q)),▸*], - exact sorry + xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))], +-- esimp, --doesn't fold elim_inclt back. The following tactic is just a "custom esimp" + xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) + (t ⬝r t'⁻¹ʳ)} + idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2)) + (inclt t) (inclt t')⁻¹ ⬝ + (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t ◾ + (ap_inv (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2)) + (inclt t') ⬝ + inverse2 (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t')))),▸*], + rewrite [-con.assoc _ _ (con_inv_eq_idp _),-con.assoc _ _ (_ ◾ _),con.assoc _ _ (ap_con _ _ _), + con.left_inv,↑whisker_left,con2_con_con2,-con.assoc (ap_inv _ _)⁻¹, + con.left_inv,+idp_con,eq_of_con_inv_eq_idp_con2], + xrewrite [to_left_inv !eq_equiv_con_inv_eq_idp (P2 q)], + apply top_deg_square end --/ end end two_quotient diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 9a9a39f9c..638f9676d 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -167,14 +167,14 @@ namespace is_equiv -- once pulled back along an equivalence f : A → B, then it has a section -- over all of B. - definition equiv_rect (P : B → Type) : + definition is_equiv_rect (P : B → Type) : (Πx, P (f x)) → (Πy, P y) := (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y))) - definition equiv_rect_comp (P : B → Type) - (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := + definition is_equiv_rect_comp (P : B → Type) + (df : Π (x : A), P (f x)) (x : A) : is_equiv_rect f P df (f x) = df x := calc - equiv_rect f P df (f x) + is_equiv_rect f P df (f x) = right_inv f (f x) ▸ df (f⁻¹ (f x)) : by esimp ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj ... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -transport_compose @@ -285,6 +285,20 @@ namespace equiv definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _ + definition equiv_rect (f : A ≃ B) (P : B → Type) : + (Πx, P (f x)) → (Πy, P y) := + (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y))) + + definition equiv_rect_comp (f : A ≃ B) (P : B → Type) + (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := + calc + equiv_rect f P df (f x) + = right_inv f (f x) ▸ df (f⁻¹ (f x)) : by esimp + ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj + ... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -transport_compose + ... = df x : by rewrite (apd df (left_inv f x)) + + namespace ops postfix `⁻¹` := equiv.symm -- overloaded notation for inverse end ops diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 3680eb7c0..5d8774f85 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -165,10 +165,10 @@ namespace eq 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 - definition con_inv_eq_idp {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp := + definition con_inv_eq_idp [unfold 6] {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp := by cases r;apply con.right_inv - definition inv_con_eq_idp {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp := + definition inv_con_eq_idp [unfold 6] {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp := by cases r;apply con.left_inv definition con_eq_idp {p : x = y} {q : y = x} (r : p = q⁻¹) : p ⬝ q = idp := @@ -544,7 +544,7 @@ namespace eq /- The 2-dimensional groupoid structure -/ -- Horizontal composition of 2-dimensional paths. - definition concat2 {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') + definition concat2 [unfold 9 10] {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') : p ⬝ q = p' ⬝ q' := eq.rec_on h (eq.rec_on h' idp) diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 8c3be3fb5..4454334f4 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -62,7 +62,7 @@ namespace eq by cases p;exact idpo definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := - pathover_of_eq_tr idp + by cases p;exact idpo definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ := pathover.rec_on r₂ r @@ -237,7 +237,7 @@ namespace eq : 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₂ := + definition change_path [unfold 9] (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ := by induction q;exact r definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ := diff --git a/hott/types/cubical/cube.hlean b/hott/types/cubical/cube.hlean index 8951aca56..16e6824e3 100644 --- a/hott/types/cubical/cube.hlean +++ b/hott/types/cubical/cube.hlean @@ -47,7 +47,7 @@ namespace eq definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) : transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ = - whisker_square (eq_bottom_of_square s₀₁₁) (eq_bottom_of_square s₂₁₁) idp idp s₁₁₂ := + whisker_square (eq_bot_of_square s₀₁₁) (eq_bot_of_square s₂₁₁) idp idp s₁₁₂ := by induction c; reflexivity --set_option pp.implicit true diff --git a/hott/types/cubical/square.hlean b/hott/types/cubical/square.hlean index c8b6d2fee..f1ecce4de 100644 --- a/hott/types/cubical/square.hlean +++ b/hott/types/cubical/square.hlean @@ -134,7 +134,7 @@ namespace eq 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 eq_bottom_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + definition eq_bot_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : p₁₂ = p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ := by induction s₁₁; apply idp @@ -165,6 +165,10 @@ namespace eq : square (l ⬝ b ⬝ r⁻¹) b l r := by induction r;induction b;induction l;constructor + definition bot_deg_square (l : a₁ = a₂) (t : a₁ = a₃) (r : a₃ = a₄) + : square t (l⁻¹ ⬝ t ⬝ r) l r := + by induction r;induction t;induction l;constructor + /- the following two equivalences have as underlying inverse function the functions hdeg_square and vdeg_square, respectively. diff --git a/hott/types/cubical/squareover.hlean b/hott/types/cubical/squareover.hlean index d01cd2910..6b5652abd 100644 --- a/hott/types/cubical/squareover.hlean +++ b/hott/types/cubical/squareover.hlean @@ -60,8 +60,8 @@ namespace eq : squareover B vrfl q₁₀ q₁₀' idpo idpo := by induction r;exact vrflo - definition hdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀') - : squareover B hrfl idpo idpo q₁₀ q₁₀' := + definition hdeg_squareover {q₀₁' : b₀₀ =[p₀₁] b₀₂} (r : q₀₁ = q₀₁') + : squareover B hrfl idpo idpo q₀₁ q₀₁' := by induction r; exact hrflo -- relating squareovers to squares @@ -120,6 +120,22 @@ namespace eq : 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_of_eq_top (r : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ) + : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ := + begin + induction s₁₁, revert q₁₂ q₁₀ r, + eapply idp_rec_on q₂₁, clear q₂₁, + intro q₁₂, + eapply idp_rec_on q₁₂, clear q₁₂, + esimp, intros, + induction r, eapply idp_rec_on q₁₀, + constructor + end + + definition eq_top_of_squareover (r : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) + : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ := + by induction r; reflexivity + /- definition squareover_equiv_pathover (q₁₀ : b₀₀ =[p₁₀] b₂₀) (q₁₂ : b₀₂ =[p₁₂] b₂₂) (q₀₁ : b₀₀ =[p₀₁] b₀₂) (q₂₁ : b₂₀ =[p₂₁] b₂₂) @@ -156,6 +172,8 @@ namespace eq (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 + begin + induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s + end end eq diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index c3cb79d91..d4281124c 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -252,7 +252,7 @@ namespace eq definition eq_equiv_eq_closed [constructor] (p : a₁ = a₂) (q : a₃ = a₄) : (a₁ = a₃) ≃ (a₂ = a₄) := equiv.trans (equiv_eq_closed_left a₃ p) (equiv_eq_closed_right a₂ q) - definition is_equiv_whisker_left (p : a₁ = a₂) (q r : a₂ = a₃) + definition is_equiv_whisker_left [constructor] (p : a₁ = a₂) (q r : a₂ = a₃) : is_equiv (whisker_left p : q = r → p ⬝ q = p ⬝ r) := begin fapply adjointify, @@ -269,10 +269,11 @@ namespace eq {intro s, induction s, induction q, induction p, reflexivity} end - definition eq_equiv_con_eq_con_left (p : a₁ = a₂) (q r : a₂ = a₃) : (q = r) ≃ (p ⬝ q = p ⬝ r) := + definition eq_equiv_con_eq_con_left [constructor] (p : a₁ = a₂) (q r : a₂ = a₃) + : (q = r) ≃ (p ⬝ q = p ⬝ r) := equiv.mk _ !is_equiv_whisker_left - definition is_equiv_whisker_right {p q : a₁ = a₂} (r : a₂ = a₃) + definition is_equiv_whisker_right [constructor] {p q : a₁ = a₂} (r : a₂ = a₃) : is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) := begin fapply adjointify, @@ -281,7 +282,8 @@ namespace eq {intro s, induction s, induction r, induction p, reflexivity} end - definition eq_equiv_con_eq_con_right (p q : a₁ = a₂) (r : a₂ = a₃) : (p = q) ≃ (p ⬝ r = q ⬝ r) := + definition eq_equiv_con_eq_con_right [constructor] (p q : a₁ = a₂) (r : a₂ = a₃) + : (p = q) ≃ (p ⬝ r = q ⬝ r) := equiv.mk _ !is_equiv_whisker_right /- @@ -289,7 +291,7 @@ namespace eq However, these proofs have the advantage that the inverse is definitionally equal to what we would expect -/ - definition is_equiv_con_eq_of_eq_inv_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) + definition is_equiv_con_eq_of_eq_inv_con [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_eq_of_eq_inv_con : p = r⁻¹ ⬝ q → r ⬝ p = q) := begin fapply adjointify, @@ -300,11 +302,11 @@ namespace eq con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end - definition eq_inv_con_equiv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) + definition eq_inv_con_equiv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : (p = r⁻¹ ⬝ q) ≃ (r ⬝ p = q) := equiv.mk _ !is_equiv_con_eq_of_eq_inv_con - definition is_equiv_con_eq_of_eq_con_inv (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) + definition is_equiv_con_eq_of_eq_con_inv [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_eq_of_eq_con_inv : r = q ⬝ p⁻¹ → r ⬝ p = q) := begin fapply adjointify, @@ -313,11 +315,11 @@ namespace 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 : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) + definition eq_con_inv_equiv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁) : (r = q ⬝ p⁻¹) ≃ (r ⬝ p = q) := equiv.mk _ !is_equiv_con_eq_of_eq_con_inv - definition is_equiv_inv_con_eq_of_eq_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) + definition is_equiv_inv_con_eq_of_eq_con [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) : is_equiv (inv_con_eq_of_eq_con : p = r ⬝ q → r⁻¹ ⬝ p = q) := begin fapply adjointify, @@ -328,11 +330,11 @@ namespace eq con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] }, end - definition eq_con_equiv_inv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) + definition eq_con_equiv_inv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂) : (p = r ⬝ q) ≃ (r⁻¹ ⬝ p = q) := equiv.mk _ !is_equiv_inv_con_eq_of_eq_con - definition is_equiv_con_inv_eq_of_eq_con (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁) + definition is_equiv_con_inv_eq_of_eq_con [constructor] (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁) : is_equiv (con_inv_eq_of_eq_con : r = q ⬝ p → r ⬝ p⁻¹ = q) := begin fapply adjointify, @@ -366,6 +368,32 @@ namespace eq : is_equiv (eq_inv_con_of_con_eq : r ⬝ p = q → p = r⁻¹ ⬝ q) := is_equiv_inv con_eq_of_eq_inv_con + definition is_equiv_con_inv_eq_idp [constructor] (p q : a₁ = a₂) + : is_equiv (con_inv_eq_idp : p = q → p ⬝ q⁻¹ = idp) := + begin + fapply adjointify, + { apply eq_of_con_inv_eq_idp}, + { intro s, induction q, esimp at *, cases s, reflexivity}, + { intro s, induction s, induction p, reflexivity}, + end + + definition is_equiv_inv_con_eq_idp [constructor] (p q : a₁ = a₂) + : is_equiv (inv_con_eq_idp : p = q → q⁻¹ ⬝ p = idp) := + begin + fapply adjointify, + { apply eq_of_inv_con_eq_idp}, + { intro s, induction q, esimp [eq_of_inv_con_eq_idp] at *, + eapply is_equiv_rect (eq_equiv_con_eq_con_left idp p idp), clear s, + intro s, cases s, reflexivity}, + { intro s, induction s, induction p, reflexivity}, + end + + definition eq_equiv_con_inv_eq_idp [constructor] (p q : a₁ = a₂) : (p = q) ≃ (p ⬝ q⁻¹ = idp) := + equiv.mk _ !is_equiv_con_inv_eq_idp + + definition eq_equiv_inv_con_eq_idp [constructor] (p q : a₁ = a₂) : (p = q) ≃ (q⁻¹ ⬝ p = idp) := + equiv.mk _ !is_equiv_inv_con_eq_idp + /- Pathover Equivalences -/ definition pathover_eq_equiv_l (p : a₁ = a₂) (q : a₁ = a₃) (r : a₂ = a₃) : q =[p] r ≃ q = p ⬝ r := diff --git a/hott/types/eq2.hlean b/hott/types/eq2.hlean index a33a05ac3..33906e227 100644 --- a/hott/types/eq2.hlean +++ b/hott/types/eq2.hlean @@ -96,6 +96,11 @@ namespace eq := by induction q;esimp at *;cases r;reflexivity + theorem eq_of_con_inv_eq_idp_con2 {p p' q q' : a₁ = a₂} (r : p = p') (s : q = q') + (t : p' ⬝ q'⁻¹ = idp) + : eq_of_con_inv_eq_idp (r ◾ inverse2 s ⬝ t) = r ⬝ eq_of_con_inv_eq_idp t ⬝ s⁻¹ := + by induction s;induction r;induction q;reflexivity + -- definition naturality_apdo {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} -- (H : f ~ g) (p : a = a₂) -- : squareover B vrfl (apdo f p) (apdo g p) diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index f5b96d7ee..6a23b1169 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -159,7 +159,7 @@ namespace pi : ap (pi_functor f0 f1) (eq_of_homotopy h) = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) := begin - apply (equiv_rect (@apd10 A B g g')), intro p, clear h, + apply (is_equiv_rect (@apd10 A B g g')), intro p, clear h, cases p, apply concat, exact (ap (ap (pi_functor f0 f1)) (eq_of_homotopy_idp g)),