From dc37ec954d18d4c74350cadec0d49de55dec41bd Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 19 Mar 2016 11:25:08 -0400 Subject: [PATCH] refactor(hott): rename apdo to apd --- hott/algebra/e_closure.hlean | 8 ++++---- hott/cubical/pathover2.hlean | 24 ++++++++++++------------ hott/cubical/squareover.hlean | 6 +++--- hott/eq2.hlean | 6 +++--- hott/hit/coeq.hlean | 4 ++-- hott/hit/colimit.hlean | 8 ++++---- hott/hit/pushout.hlean | 4 ++-- hott/hit/quotient.hlean | 6 +++--- hott/hit/refl_quotient.hlean | 2 +- hott/hit/set_quotient.hlean | 4 ++-- hott/hit/two_quotient.hlean | 24 ++++++++++++------------ hott/homotopy/circle.hlean | 20 ++++++++++---------- hott/homotopy/cylinder.hlean | 4 ++-- hott/homotopy/interval.hlean | 4 ++-- hott/homotopy/join.hlean | 8 ++++---- hott/homotopy/red_susp.hlean | 2 +- hott/homotopy/susp.hlean | 6 +++--- hott/homotopy/torus.hlean | 4 ++-- hott/init/hit.hlean | 2 +- hott/init/pathover.hlean | 20 ++++++++++---------- hott/types/sigma.hlean | 2 +- hott/types/univ.hlean | 2 +- tests/lean/extra/755.hlean | 4 ++-- 23 files changed, 87 insertions(+), 87 deletions(-) diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean index 46b5c3cb7..3048e6938 100644 --- a/hott/algebra/e_closure.hlean +++ b/hott/algebra/e_closure.hlean @@ -171,15 +171,15 @@ section definition ap_e_closure_elimo_h [unfold 12] {g' : Πb, Q (g b)} (p : Π⦃a a' : A⦄, R a a' → f a = f a') (po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a')) - (q : Π⦃a a' : A⦄ (s : R a a'), apdo g' (p s) = po s) - (t : T a a') : apdo g' (e_closure.elim p t) = e_closure.elimo p po t := + (q : Π⦃a a' : A⦄ (s : R a a'), apd g' (p s) = po s) + (t : T a a') : apd g' (e_closure.elim p t) = e_closure.elimo p po t := begin induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂, apply q, induction pp, reflexivity, esimp [e_closure.elim], - exact apdo_inv g' (e_closure.elim p r) ⬝ IH⁻²ᵒ, - exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂) + exact apd_inv g' (e_closure.elim p r) ⬝ IH⁻²ᵒ, + exact apd_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂) end theorem e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))} diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean index 193ac69c7..e0a41b123 100644 --- a/hott/cubical/pathover2.hlean +++ b/hott/cubical/pathover2.hlean @@ -37,8 +37,8 @@ namespace eq : pathover_of_tr_eq r = pathover_tr p b ⬝o pathover_idp_of_eq r := by induction r; induction p; reflexivity - definition apo011_eq_apo11_apdo (f : Πa, B a → A') (p : a = a₂) (q : b =[p] b₂) - : apo011 f p q = eq_of_pathover (apo11 (apdo f p) q) := + definition apo011_eq_apo11_apd (f : Πa, B a → A') (p : a = a₂) (q : b =[p] b₂) + : apo011 f p q = eq_of_pathover (apo11 (apd f p) q) := by induction q; reflexivity definition change_path_con (q : p = p') (q' : p' = p'') (r : b =[p] b₂) : @@ -92,23 +92,23 @@ namespace eq { intro r, induction q, reflexivity}, end - definition apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) - : apdo g (ap f p) = pathover_ap B f (apdo (λx, g (f x)) p) := + definition apd_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) + : apd g (ap f p) = pathover_ap B f (apd (λx, g (f x)) p) := by induction p; reflexivity - definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) - : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) := + definition apd_eq_apd_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂) + : apd (λx, g (f x)) p = pathover_of_pathover_ap B f (apd g (ap f p)) := by induction p; reflexivity definition ap_compose_ap02_constant {A B C : Type} {a a' : A} (p : a = a') (b : B) (c : C) : ap_compose (λc, b) (λa, c) p ⬝ ap02 (λc, b) (ap_constant p c) = ap_constant p b := by induction p; reflexivity - theorem apdo_constant (b : B'' a') (p : a = a) : - pathover_ap B'' (λa, a') (apdo (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo := + theorem apd_constant (b : B'' a') (p : a = a) : + pathover_ap B'' (λa, a') (apd (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo := begin - rewrite [apdo_eq_apdo_ap _ _ p], - let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ, + rewrite [apd_eq_apd_ap _ _ p], + let y := !change_path_of_pathover (apd (apd id) (ap_constant p b))⁻¹ᵒ, rewrite -y, esimp, refine !pathover_ap_pathover_of_pathover_ap ⬝ _, rewrite pathover_ap_change_path, @@ -117,8 +117,8 @@ namespace eq apply ap_compose_ap02_constant end - definition apdo_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p') - : apdo f p' = change_path s (apdo f p) := + definition apd_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p') + : apd f p' = change_path s (apd f p) := by induction s; reflexivity definition cono_invo_eq_idpo {q q' : b =[p] b₂} (r : q = q') diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean index e3d048487..8abf3f3ff 100644 --- a/hott/cubical/squareover.hlean +++ b/hott/cubical/squareover.hlean @@ -49,7 +49,7 @@ namespace eq definition idso [reducible] [constructor] := @squareover.idsquareo A B a₀₀ b₀₀ definition apds (f : Πa, B a) (s : square p₁₀ p₁₂ p₀₁ p₂₁) - : squareover B s (apdo f p₁₀) (apdo f p₁₂) (apdo f p₀₁) (apdo f p₂₁) := + : squareover B s (apd f p₁₀) (apd f p₁₂) (apd f p₀₁) (apd f p₂₁) := square.rec_on s idso definition vrflo : squareover B vrfl q₁₀ q₁₀ idpo idpo := @@ -244,7 +244,7 @@ namespace eq /- A version of eq_pathover where the type of the equality also varies -/ definition eq_pathover_dep {f g : Πa, B a} {p : a = a'} {q : f a = g a} {r : f a' = g a'} (s : squareover B hrfl (pathover_idp_of_eq q) (pathover_idp_of_eq r) - (apdo f p) (apdo g p)) : q =[p] r := + (apd f p) (apd g p)) : q =[p] r := begin induction p, apply pathover_idp_of_eq, apply eq_of_vdeg_square, exact square_of_squareover_ids s end @@ -256,7 +256,7 @@ namespace eq (r : pathover B (b a') (q a') (b₂ a')) (r₂ : pathover B (b a₂') (q a₂') (b₂ a₂')) (s : squareover B (natural_square_tr q p) r r₂ - (pathover_ap B f (apdo b p)) (pathover_ap B g (apdo b₂ p))) + (pathover_ap B f (apd b p)) (pathover_ap B g (apd b₂ p))) : pathover (λa, pathover B (b a) (q a) (b₂ a)) r p r₂ := begin induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s diff --git a/hott/eq2.hlean b/hott/eq2.hlean index 493ab7d79..556398361 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -14,7 +14,7 @@ namespace eq theorem ap_is_constant_eq (p : Πx, f x = b) (q : a = a') : ap_is_constant p q = - eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apdo p q)))⁻¹ ⬝ + eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apd p q)))⁻¹ ⬝ whisker_left (p a) (ap_constant q b)) := begin induction q, esimp, generalize (p a), intro p, cases p, apply idpath idp @@ -105,9 +105,9 @@ namespace eq : 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_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} + definition naturality_apd_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a} (H : f ~ g) (p : a = a₂) - : apdo f p = concato_eq (eq_concato (H a) (apdo g p)) (H a₂)⁻¹ := + : apd f p = concato_eq (eq_concato (H a) (apd g p)) (H a₂)⁻¹ := begin induction p, esimp, generalizes [H a, g a], intro ga Ha, induction Ha, diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index d10da154c..d88138c9a 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -44,7 +44,7 @@ parameters {A B : Type.{u}} (f g : A → B) theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) - (x : A) : apdo (rec P_i Pcp) (cp x) = Pcp x := + (x : A) : apd (rec P_i Pcp) (cp x) = Pcp x := !rec_eq_of_rel protected definition elim {P : Type} (P_i : B → P) @@ -59,7 +59,7 @@ parameters {A B : Type.{u}} (f g : A → B) (x : A) : ap (elim P_i Pcp) (cp x) = Pcp x := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (cp x)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cp], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cp], end protected definition elim_type (P_i : B → Type) diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index f877f4a96..a9d2fd38e 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -50,7 +50,7 @@ section theorem rec_cglue {P : colimit → Type} (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) - {j : J} (x : A (dom j)) : apdo (rec Pincl Pglue) (cglue j x) = Pglue j x := + {j : J} (x : A (dom j)) : apd (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) @@ -68,7 +68,7 @@ section {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cglue], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cglue], end protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type) @@ -141,7 +141,7 @@ section theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) {n : ℕ} (a : A n) - : apdo (rec Pincl Pglue) (glue a) = Pglue a := + : apd (rec Pincl Pglue) (glue a) = Pglue a := !rec_eq_of_rel protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P) @@ -158,7 +158,7 @@ section : ap (elim Pincl Pglue) (glue a) = Pglue a := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_glue], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_glue], end protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type) diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index f9fd7d51e..4efe06248 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -51,7 +51,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x)) - (x : TL) : apdo (rec Pinl Pinr Pglue) (glue x) = Pglue x := + (x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x := !rec_eq_of_rel protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P) @@ -67,7 +67,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) : ap (elim Pinl Pinr Pglue) (glue x) = Pglue x := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (glue x)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue], end protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type) diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 1663af705..94968740c 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -35,7 +35,7 @@ namespace quotient : ap (quotient.elim Pc Pp) (eq_of_rel R H) = Pp H := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel], end protected definition rec_prop {A : Type} {R : A → A → Type} {P : quotient R → Type} @@ -89,7 +89,7 @@ namespace quotient (Σ(f : Π(a : A), C (class_of R a)), Π⦃a a' : A⦄ (H : R a a'), f a =[eq_of_rel R H] f a') := begin fapply equiv.MK, - { intro f, exact ⟨λa, f (class_of R a), λa a' H, apdo f (eq_of_rel R H)⟩}, + { intro f, exact ⟨λa, f (class_of R a), λa a' H, apd f (eq_of_rel R H)⟩}, { intro v x, induction v with i p, induction x, exact (i a), exact (p H)}, @@ -166,7 +166,7 @@ namespace quotient (c : C a) : ap (elim @Qpt Qeq) (Peq r c) = Qeq r c := begin refine !ap_dpair_eq_dpair ⬝ _, - rewrite [apo011_eq_apo11_apdo, rec_eq_of_rel, ▸*, apo011_arrow_pathover_constant_right, + rewrite [apo011_eq_apo11_apd, rec_eq_of_rel, ▸*, apo011_arrow_pathover_constant_right, ↑elim_type_eq_of_rel', to_right_inv !pathover_equiv_tr_eq, ap_inv], apply inv_con_cancel_right end diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean index 3f5cc05e1..010a30705 100644 --- a/hott/hit/refl_quotient.hlean +++ b/hott/hit/refl_quotient.hlean @@ -47,7 +47,7 @@ section definition rec_req_of_rel {P : Type} {P : refl_quotient → Type} (Pc : Π(a : A), P (rclass_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a') (Pr : Π(a : A), change_path (pρ a) (Pp (ρ a)) = idpo) ⦃a a' : A⦄ (r : R a a') - : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r := + : apd (rec Pc Pp Pr) (req_of_rel r) = Pp r := !rec_incl1 protected definition elim {P : Type} (Pc : Π(a : A), P) diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean index 9b75b648e..5b0574174 100644 --- a/hott/hit/set_quotient.hlean +++ b/hott/hit/set_quotient.hlean @@ -44,7 +44,7 @@ section theorem rec_eq_of_rel {P : set_quotient → Type} [Pt : Πaa, is_set (P aa)] (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') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H := + {a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H := !is_set.elimo protected definition elim {P : Type} [Pt : is_set P] (Pc : A → P) @@ -60,7 +60,7 @@ section : ap (elim Pc Pp) (eq_of_rel H) = Pp H := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], end protected definition rec_prop {P : set_quotient → Type} [Pt : Πaa, is_prop (P aa)] diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index e96e346da..baafed5b9 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -76,7 +76,7 @@ namespace simple_two_quotient protected theorem rec_e {P : C → Type} (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q)) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (s : R a a') - : apdo (pre_rec Pj Pa Pe) (e s) = Pe s := + : apd (pre_rec Pj Pa Pe) (e s) = Pe s := !rec_eq_of_rel protected theorem elim_e {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) @@ -84,7 +84,7 @@ namespace simple_two_quotient : ap (pre_elim Pj Pa Pe) (e s) = Pe s := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pre_elim,rec_e], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pre_elim,rec_e], end protected definition elim_et {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P) @@ -95,7 +95,7 @@ namespace simple_two_quotient protected definition rec_et {P : C → Type} (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q)) (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (t : T a a') - : apdo (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t := + : apd (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t := ap_e_closure_elimo_h e Pe (rec_e Pj Pa Pe) t inductive simple_two_quotient_rel : C → C → Type := @@ -151,9 +151,9 @@ namespace simple_two_quotient refine eq_hconcato _ _, apply _, { transitivity _, { apply ap (pathover_ap _ _), - transitivity _, apply apdo_compose2 (pre_rec P0 _ _) (f q) loop, + transitivity _, apply apd_compose2 (pre_rec P0 _ _) (f q) loop, apply ap (pathover_of_pathover_ap _ _), - transitivity _, apply apdo_change_path, exact !elim_loop⁻¹, + transitivity _, apply apd_change_path, exact !elim_loop⁻¹, transitivity _, apply ap (change_path _), transitivity _, apply rec_et, @@ -171,7 +171,7 @@ namespace simple_two_quotient rewrite [↑incl2, con_inv], transitivity _, exact !con.assoc⁻¹, rewrite [inv_con_cancel_right, ↑incl2w, ↑ap02, +con_inv, +ap_inv, +inv_inv, -+con.assoc, +con_inv_cancel_right], reflexivity}, - rewrite [change_path_con, apdo_constant], + rewrite [change_path_con, apd_constant], apply squareover_change_path_left, apply squareover_change_path_right', apply squareover_change_path_left, refine change_square _ vrflo, @@ -189,9 +189,9 @@ namespace simple_two_quotient (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (s : R a a') - : apdo (rec P0 P1 P2) (incl1 s) = P1 s := + : apd (rec P0 P1 P2) (incl1 s) = P1 s := begin - unfold [rec, incl1], refine !apdo_ap ⬝ _, esimp, rewrite rec_e, + unfold [rec, incl1], refine !apd_ap ⬝ _, esimp, rewrite rec_e, apply to_right_inv !pathover_compose end @@ -199,7 +199,7 @@ namespace simple_two_quotient (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (t : T a a') - : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := + : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t protected definition elim {P : Type} (P0 : A → P) @@ -288,7 +288,7 @@ namespace simple_two_quotient ↑[elim_incltw]], apply whisker_tl, rewrite [ap_is_constant_eq], - xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop], + xrewrite [naturality_apd_eq (λx, !elim_eq_of_rel) loop], rewrite [↑elim_2,rec_loop,square_of_pathover_concato_eq,square_of_pathover_eq_concato, eq_of_square_vconcat_eq,eq_of_square_eq_vconcat], apply eq_vconcat, @@ -390,14 +390,14 @@ namespace two_quotient (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') - ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s := + ⦃a a' : A⦄ (s : R a a') : apd (rec P0 P1 P2) (incl1 s) = P1 s := rec_incl1 _ _ _ s theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a)) (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a') (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') - ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := + ⦃a a' : A⦄ (t : T a a') : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t := rec_inclt _ _ _ t protected definition elim {P : Type} (P0 : A → P) diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 8c810a98a..e257d97be 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -42,12 +42,12 @@ namespace circle theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) - : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := + : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := !rec_merid theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) - : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := + : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := !rec_merid definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 Ps2 : Pb1 = Pb2) (x : circle) : P := @@ -61,14 +61,14 @@ namespace circle : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := begin apply eq_of_fn_eq_fn_inv !(pathover_constant seg1), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg1], + rewrite [▸*,-apd_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 eq_of_fn_eq_fn_inv !(pathover_constant seg2), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg2], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg2], end definition elim2_type (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2) (x : circle) : Type := @@ -109,9 +109,9 @@ namespace circle eq.rec_on p idp theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) : - apdo (circle.rec Pbase Ploop) loop = Ploop := + apd (circle.rec Pbase Ploop) loop = Ploop := begin - rewrite [↑loop,apdo_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apdo_inv,rec2_seg1], + rewrite [↑loop,apd_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apd_inv,rec2_seg1], apply rec_loop_helper end @@ -127,14 +127,14 @@ namespace circle ap (circle.elim Pbase Ploop) loop = Ploop := begin apply eq_of_fn_eq_fn_inv !(pathover_constant loop), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,rec_loop], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,rec_loop], end theorem elim_seg1 {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : ap (circle.elim Pbase Ploop) seg1 = (tr_constant seg1 Pbase)⁻¹ := begin apply eq_of_fn_eq_fn_inv !(pathover_constant seg1), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], rewrite [↑circle.rec2_on,rec2_seg1], apply inverse, apply pathover_of_eq_tr_constant_inv end @@ -143,7 +143,7 @@ namespace circle : ap (circle.elim Pbase Ploop) seg2 = Ploop ⬝ (tr_constant seg1 Pbase)⁻¹ := begin apply eq_of_fn_eq_fn_inv !(pathover_constant seg2), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec], rewrite [↑circle.rec2_on,rec2_seg2], assert l : Π(A B : Type)(a a₂ a₂' : A)(b b' : B)(p : a = a₂)(p' : a₂' = a₂) (q : b = b'), @@ -188,7 +188,7 @@ namespace circle : (Π(x : S¹), P x) ≃ Σ(p : P base), p =[loop] p := begin fapply equiv.MK, - { intro f, exact ⟨f base, apdo f loop⟩}, + { intro f, exact ⟨f base, apd f loop⟩}, { intro v x, induction v with p q, induction x, { exact p}, { exact q}}, diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean index 62f661c67..410da225f 100644 --- a/hott/homotopy/cylinder.hlean +++ b/hott/homotopy/cylinder.hlean @@ -52,7 +52,7 @@ parameters {A B : Type.{u}} (f : A → B) theorem rec_seg {P : cylinder → Type} (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a)) (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a) - (a : A) : apdo (rec Pbase Ptop Pseg) (seg a) = Pseg a := + (a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a := !rec_eq_of_rel protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P) @@ -68,7 +68,7 @@ parameters {A B : Type.{u}} (f : A → B) (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_seg], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_seg], end protected definition elim_type (Pbase : B → Type) (Ptop : A → Type) diff --git a/hott/homotopy/interval.hlean b/hott/homotopy/interval.hlean index 154511c4e..c25e103f3 100644 --- a/hott/homotopy/interval.hlean +++ b/hott/homotopy/interval.hlean @@ -31,7 +31,7 @@ namespace interval interval.rec P0 P1 Ps x theorem rec_seg {P : interval → Type} (P0 : P zero) (P1 : P one) (Ps : P0 =[seg] P1) - : apdo (interval.rec P0 P1 Ps) seg = Ps := + : apd (interval.rec P0 P1 Ps) seg = Ps := !rec_merid protected definition elim {P : Type} (P0 P1 : P) (Ps : P0 = P1) (x : interval) : P := @@ -45,7 +45,7 @@ namespace interval : ap (interval.elim P0 P1 Ps) seg = Ps := begin apply eq_of_fn_eq_fn_inv !(pathover_constant seg), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑interval.elim,rec_seg], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑interval.elim,rec_seg], end protected definition elim_type (P0 P1 : Type) (Ps : P0 ≃ P1) (x : interval) : Type := diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index b6025afcb..22c817ed5 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -34,7 +34,7 @@ namespace join (Pinr : Π(y : B), P (inr y)) (Pglue : Π(x : A)(y : B), Pinl x =[glue x y] Pinr y) (x : A) (y : B) - : apdo (join.rec Pinl Pinr Pglue) (glue x y) = Pglue x y := + : apd (join.rec Pinl Pinr Pglue) (glue x y) = Pglue x y := !quotient.rec_eq_of_rel protected definition elim {P : Type} (Pinl : A → P) (Pinr : B → P) @@ -46,7 +46,7 @@ namespace join : ap (join.elim Pinl Pinr Pglue) (glue x y) = Pglue x y := begin apply equiv.eq_of_fn_eq_fn_inv !(pathover_constant (glue x y)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑join.elim], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑join.elim], apply join.rec_glue end @@ -404,7 +404,7 @@ section join_switch private definition switch_inv_cube_aux2 {A B : Type} {b : B} {f : A → B} (g : Π a, f a = b) {x y : A} (p : x = y) {sq : square (g x) (g y) (ap f p) idp} - (q : apdo g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq := + (q : apd g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq := begin cases p, esimp at *, apply concat, apply inverse, apply vdeg_square_idp, apply concat, apply ap vdeg_square, exact ap eq_of_pathover_idp q, @@ -448,7 +448,7 @@ section join_switch private definition natural_square_tr_beta {A B : Type} {f₁ f₂ : A → B} (p : Π a, f₁ a = f₂ a) {x y : A} (q : x = y) {sq : square (p x) (p y) (ap f₁ q) (ap f₂ q)} - (e : apdo p q = eq_pathover sq) : + (e : apd p q = eq_pathover sq) : natural_square_tr p q = sq := begin cases q, esimp at *, apply concat, apply inverse, apply vdeg_square_idp, diff --git a/hott/homotopy/red_susp.hlean b/hott/homotopy/red_susp.hlean index a71996e89..b46b65a3d 100644 --- a/hott/homotopy/red_susp.hlean +++ b/hott/homotopy/red_susp.hlean @@ -47,7 +47,7 @@ section -- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) -- (Pe : Pm pt =[merid_pt] idpo) (a : A) - -- : apdo (rec Pb Pm Pe) (merid a) = Pm a := + -- : apd (rec Pb Pm Pe) (merid a) = Pm a := -- !rec_incl1 -- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb) diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index aab3ab608..ba6417966 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -39,7 +39,7 @@ namespace susp theorem rec_merid {P : susp A → Type} (PN : P north) (PS : P south) (Pm : Π(a : A), PN =[merid a] PS) (a : A) - : apdo (susp.rec PN PS Pm) (merid a) = Pm a := + : apd (susp.rec PN PS Pm) (merid a) = Pm a := !rec_glue protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) @@ -54,7 +54,7 @@ namespace susp : ap (susp.elim PN PS Pm) (merid a) = Pm a := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑susp.elim,rec_merid], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑susp.elim,rec_merid], end protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) @@ -119,7 +119,7 @@ end susp /- Flattening lemma -/ namespace susp - + open prod prod.ops section universe variable u diff --git a/hott/homotopy/torus.hlean b/hott/homotopy/torus.hlean index 3a1f55cd9..1f9da174c 100644 --- a/hott/homotopy/torus.hlean +++ b/hott/homotopy/torus.hlean @@ -51,12 +51,12 @@ namespace torus theorem rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2) - : apdo (torus.rec Pb Pl1 Pl2 Ps) loop1 = Pl1 := + : apd (torus.rec Pb Pl1 Pl2 Ps) loop1 = Pl1 := !rec_incl1 theorem rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb) (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2) - : apdo (torus.rec Pb Pl1 Pl2 Ps) loop2 = Pl2 := + : apd (torus.rec Pb Pl1 Pl2 Ps) loop2 = Pl2 := !rec_incl1 protected definition elim {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb) diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index ea3c27526..4a6197c03 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -81,7 +81,7 @@ namespace quotient constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : quotient R → Type} (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') : apdo (quotient.rec Pc Pp) (eq_of_rel R H) = Pp H + {a a' : A} (H : R a a') : apd (quotient.rec Pc Pp) (eq_of_rel R H) = Pp H end quotient attribute quotient.class_of trunc.tr [constructor] diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index bf0262850..1b96d4ebc 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -70,7 +70,7 @@ namespace eq definition inverseo [unfold 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b := pathover.rec_on r idpo - definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := + definition apd [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := eq.rec_on p idpo definition concato_eq [unfold 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' := @@ -198,15 +198,15 @@ namespace eq { intro q, cases q, reflexivity}, 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 := + definition apd_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃) + : apd f (p ⬝ q) = apd f p ⬝o apd f q := by cases p; cases q; reflexivity - definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ := + definition apd_inv (f : Πa, B a) (p : a = a₂) : apd f p⁻¹ = (apd f p)⁻¹ᵒ := by cases p; reflexivity - definition apdo_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) : - apdo f p = pathover_of_eq (ap f p) := + definition apd_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) : + apd 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₂ := @@ -273,12 +273,12 @@ namespace eq (q : b =[p] b₂) : f b =[p] g b₂ := by induction q; exact apo10 r b - definition apdo_compose1 (g : Πa, B a → B' a) (f : Πa, B a) (p : a = a₂) - : apdo (g ∘' f) p = apo g (apdo f p) := + definition apd_compose1 (g : Πa, B a → B' a) (f : Πa, B a) (p : a = a₂) + : apd (g ∘' f) p = apo g (apd f p) := by induction p; reflexivity - definition apdo_compose2 (g : Πa', B'' a') (f : A → A') (p : a = a₂) - : apdo (λa, g (f a)) p = pathover_of_pathover_ap B'' f (apdo g (ap f p)) := + definition apd_compose2 (g : Πa', B'' a') (f : A → A') (p : a = a₂) + : apd (λa, g (f a)) p = pathover_of_pathover_ap B'' f (apd g (ap f p)) := by induction p; reflexivity definition cono.right_inv_eq (q : b = b') diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 47c5b2376..b13912ad5 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -63,7 +63,7 @@ namespace sigma ap eq_pr1 r definition eq2_pr2 {p q : u = v} (r : p = q) : p..2 =[eq2_pr1 r] q..2 := - !pathover_ap (apdo eq_pr2 r) + !pathover_ap (apd eq_pr2 r) definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : u.2 =[p] v.2) : transport (λx, B' x.1) (sigma_eq p q) = transport B' p := diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index bf396ba67..f60e2fdc0 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -51,7 +51,7 @@ namespace univ begin intro f, have u : ¬¬bool, by exact (λg, g tt), - let H1 := apdo f eq_bnot, + let H1 := apd f eq_bnot, note H2 := apo10 H1 u, have p : eq_bnot ▸ u = u, from !is_prop.elim, rewrite p at H2, diff --git a/tests/lean/extra/755.hlean b/tests/lean/extra/755.hlean index 193156c89..2df1b7cd0 100644 --- a/tests/lean/extra/755.hlean +++ b/tests/lean/extra/755.hlean @@ -31,7 +31,7 @@ section theorem rec_tr_eq {P : one_step_tr → Type} (Pt : Π(a : A), P (tr a)) (Pe : Π(a a' : A), Pt a =[tr_eq a a'] Pt a') (a a' : A) - : apdo (rec Pt Pe) (tr_eq a a') = Pe a a' := + : apd (rec Pt Pe) (tr_eq a a') = Pe a a' := !rec_eq_of_rel theorem elim_tr_eq {P : Type} (Pt : A → P) @@ -39,7 +39,7 @@ section : ap (elim Pt Pe) (tr_eq a a') = Pe a a' := begin apply eq_of_fn_eq_fn_inv !(pathover_constant (tr_eq a a')), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_tr_eq], + rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq], end end