michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(hott): rename apd to apdt

Browse source
This commit is contained in:
Floris van Doorn 2016-03-19 10:38:05 -04:00 committed by Leonardo de Moura
parent b1ed69f621
commit 05b59aecf8
14 changed files with 35 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/functor/basic.hlean
View file

@ -201,7 +201,7 @@ namespace functor
by (cases F; apply functor_mk_eq'_idp)
definition functor_eq_eta' {F₁ F₂ : C ⇒ D} (p : F₁ = F₂)
: functor_eq' (ap to_fun_ob p) (!tr_compose⁻¹ ⬝ apd to_fun_hom p) = p :=
: functor_eq' (ap to_fun_ob p) (!tr_compose⁻¹ ⬝ apdt to_fun_hom p) = p :=
begin
cases p, cases F₁,
refine _ ⬝ !functor_eq'_idp,

2
hott/algebra/category/precategory.hlean
View file

@ -247,7 +247,7 @@ namespace category
definition Precategory_eq_hom [unfold 3] {C D : Precategory} (p : C = D) (a b : C)
: hom a b = hom (cast (ap carrier p) a) (cast (ap carrier p) b) :=
by induction p; reflexivity
--(ap10 (ap10 (apd (λx, @hom (carrier x) (Precategory.struct x)) p⁻¹ᵖ) a) b)⁻¹ᵖ ⬝ _
--(ap10 (ap10 (apdt (λx, @hom (carrier x) (Precategory.struct x)) p⁻¹ᵖ) a) b)⁻¹ᵖ ⬝ _
-- beta/eta rules

2
hott/arity.hlean
View file

@ -35,7 +35,7 @@ namespace eq
apdi₀i₁...iₙ.
For versions where only some arguments depend on some other arguments,
or for versions with transport in the conclusion (like apd), we don't have a
or for versions with transport in the conclusion (like apdt), we don't have a
consistent naming scheme (yet).
We don't prove each theorem systematically, but prove only the ones which we actually need.

2
hott/hit/quotient.hlean
View file

@ -137,7 +137,7 @@ namespace quotient
induction q,
{ exact Qpt p},
{ apply pi_pathover_left', esimp, intro c,
refine _ ⬝op apd Qpt (elim_type_eq_of_rel C f H c)⁻¹ᵖ,
refine _ ⬝op apdt Qpt (elim_type_eq_of_rel C f H c)⁻¹ᵖ,
refine _ ⬝op (tr_compose Q Ppt _ _)⁻¹ ,
rewrite ap_inv,
refine pathover_cancel_right _ !tr_pathover⁻¹ᵒ,

2
hott/init/default.hlean
View file

@ -19,7 +19,7 @@ namespace core
export sigma (hiding pr1 pr2)
export [notation] prod
export [notation] nat
export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apdt refl)
export [declaration] function
export equiv (to_inv to_right_inv to_left_inv)
export is_equiv (inv right_inv left_inv adjointify)

4
hott/init/equiv.hlean
View file

@ -186,7 +186,7 @@ namespace is_equiv
= 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 -tr_compose
... = df x : by rewrite (apd df (left_inv f x))
... = df x : by rewrite (apdt df (left_inv f x))
theorem adj_inv (b : B) : left_inv f (f⁻¹ b) = ap f⁻¹ (right_inv f b) :=
is_equiv_rect f _
@ -379,7 +379,7 @@ namespace equiv
= 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 -tr_compose
... = df x : by rewrite (apd df (left_inv f x))
... = df x : by rewrite (apdt df (left_inv f x))
end
section

2
hott/init/funext.hlean
View file

@ -235,7 +235,7 @@ axiom function_extensionality : funext
variables {A : Type} {P : A → Type} {f g : Π x, P x}
namespace funext
theorem is_equiv_apd [instance] (f g : Π x, P x) : is_equiv (@apd10 A P f g) :=
theorem is_equiv_apdt [instance] (f g : Π x, P x) : is_equiv (@apd10 A P f g) :=
function_extensionality f g
end funext

34
hott/init/path.hlean
View file

@ -257,7 +257,7 @@ namespace eq
definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
by induction H; exact ap f p
definition apd [unfold 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y :=
definition apdt [unfold 6] (f : Πa, P a) {x y : A} (p : x = y) : p ▸ f x = f y :=
by induction p; reflexivity
definition ap011 [unfold 9] (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
@ -456,16 +456,16 @@ namespace eq
tr_inv_tr p (transport P p z) = ap (transport P p) (inv_tr_tr p z) :=
by induction p; reflexivity
/- some properties for apd -/
/- some properties for apdt -/
definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp
definition apdt_idp (x : A) (f : Πx, P x) : apdt f idp = idp :> (f x = f x) := idp
definition apd_con (f : Πx, P x) {x y z : A} (p : x = y) (q : y = z)
: apd f (p ⬝ q) = con_tr p q (f x) ⬝ ap (transport P q) (apd f p) ⬝ apd f q :=
definition apdt_con (f : Πx, P x) {x y z : A} (p : x = y) (q : y = z)
: apdt f (p ⬝ q) = con_tr p q (f x) ⬝ ap (transport P q) (apdt f p) ⬝ apdt f q :=
by cases p; cases q; apply idp
definition apd_inv (f : Πx, P x) {x y : A} (p : x = y)
: apd f p⁻¹ = (eq_inv_tr_of_tr_eq (apd f p))⁻¹ :=
definition apdt_inv (f : Πx, P x) {x y : A} (p : x = y)
: apdt f p⁻¹ = (eq_inv_tr_of_tr_eq (apdt f p))⁻¹ :=
by cases p; apply idp
@ -562,11 +562,11 @@ namespace eq
definition tr_eq_cast_ap_fn {P : A → Type} {x y} (p : x = y) : transport P p = cast (ap P p) :=
by induction p; reflexivity
/- The behavior of [ap] and [apd] -/
/- The behavior of [ap] and [apdt] -/
-- In a constant fibration, [apd] reduces to [ap], modulo [transport_const].
definition apd_eq_tr_constant_con_ap (f : A → B) (p : x = y) :
apd f p = tr_constant p (f x) ⬝ ap f p :=
-- In a constant fibration, [apdt] reduces to [ap], modulo [transport_const].
definition apdt_eq_tr_constant_con_ap (f : A → B) (p : x = y) :
apdt f p = tr_constant p (f x) ⬝ ap f p :=
by induction p; reflexivity
@ -708,17 +708,17 @@ namespace eq
⬝ (ap_con f p' q')⁻¹ :=
by induction r; induction s; induction q; induction p; reflexivity
definition apd02 [unfold 8] {p q : x = y} (f : Π x, P x) (r : p = q) :
apd f p = transport2 P r (f x) ⬝ apd f q :=
definition apdt02 [unfold 8] {p q : x = y} (f : Π x, P x) (r : p = q) :
apdt f p = transport2 P r (f x) ⬝ apdt f q :=
by induction r; exact !idp_con⁻¹
-- And now for a lemma whose statement is much longer than its proof.
definition apd02_con {P : A → Type} (f : Π x:A, P x) {x y : A}
definition apdt02_con {P : A → Type} (f : Π x:A, P x) {x y : A}
{p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) :
apd02 f (r1 ⬝ r2) = apd02 f r1
⬝ whisker_left (transport2 P r1 (f x)) (apd02 f r2)
apdt02 f (r1 ⬝ r2) = apdt02 f r1
⬝ whisker_left (transport2 P r1 (f x)) (apdt02 f r2)
⬝ con.assoc' _ _ _
⬝ (whisker_right (tr2_con r1 r2 (f x))⁻¹ (apd f p3)) :=
⬝ (whisker_right (tr2_con r1 r2 (f x))⁻¹ (apdt f p3)) :=
by induction r2; induction r1; induction p1; reflexivity
end eq

4
hott/types/eq.hlean
View file

@ -151,7 +151,7 @@ namespace eq
definition transport_eq_FlFr_D {B : A → Type} {f g : Πa, B a}
(p : a₁ = a₂) (q : f a₁ = g a₁)
: transport (λx, f x = g x) p q = (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) :=
: transport (λx, f x = g x) p q = (apdt f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apdt g p) :=
by induction p; rewrite [▸*,idp_con,ap_id]
definition transport_eq_FFlr (p : a₁ = a₂) (q : h (f a₁) = a₁)
@ -189,7 +189,7 @@ namespace eq
by induction p; rewrite [▸*,idp_con]; exact idpo
definition pathover_eq_FlFr_D {B : A → Type} {f g : Πa, B a} (p : a₁ = a₂) (q : f a₁ = g a₁)
: q =[p] (apd f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apd g p) := /-(λx, f x = g x)-/
: q =[p] (apdt f p)⁻¹ ⬝ ap (transport B p) q ⬝ (apdt g p) := /-(λx, f x = g x)-/
by induction p; rewrite [▸*,idp_con,ap_id];exact idpo
definition pathover_eq_FFlr (p : a₁ = a₂) (q : h (f a₁) = a₁) : q =[p] (ap h (ap f p))⁻¹ ⬝ q ⬝ p :=

4
hott/types/pi.hlean
View file

@ -215,12 +215,12 @@ namespace pi
begin
intro h, apply eq_of_homotopy, intro a', esimp,
rewrite [adj f0 a',-tr_compose,fn_tr_eq_tr_fn _ f1,right_inv (f1 _)],
apply apd
apply apdt
end,
begin
intro h, apply eq_of_homotopy, intro a, esimp,
rewrite [left_inv (f1 _)],
apply apd
apply apdt
end
end

2
hott/types/trunc.hlean
View file

@ -281,7 +281,7 @@ namespace is_trunc
(imp : Π{a b : A}, R a b → a = b) : is_set A :=
is_set_of_axiom_K
(λa p,
have H2 : transport (λx, R a x → a = x) p (@imp a a) = @imp a a, from !apd,
have H2 : transport (λx, R a x → a = x) p (@imp a a) = @imp a a, from !apdt,
have H3 : Π(r : R a a), transport (λx, a = x) p (imp r)
= imp (transport (λx, R a x) p r), from
to_fun (equiv.symm !heq_pi) H2,

2
tests/lean/531.hlean
View file

@ -52,7 +52,7 @@ namespace colimit
definition comp_cglue [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
{j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
{j : Ihom} (x : ob (dom j)) : apdt (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
--the sorry's in the statement can be removed when comp_incl is definitional
sorry --idp

6
tests/lean/hott/433.hlean
View file

@ -38,7 +38,7 @@ namespace pi
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
definition path_equiv_homotopy (H : funext) (f g : Πx, B x) : (f = g) ≃ (f ~ g) :=
equiv.mk _ !is_equiv_apd
equiv.mk _ !is_equiv_apdt
definition is_equiv_path_pi [instance] (H : funext) (f g : Πx, B x)
: is_equiv (@eq_of_homotopy _ _ f g) :=
@ -111,11 +111,11 @@ namespace pi
rewrite -tr_compose,
rewrite {f1 a' _}(fn_tr_eq_tr_fn _ f1 _),
rewrite (right_inv (f1 _) _),
apply apd,
apply apdt,
intro h,
apply eq_of_homotopy, intro a, esimp,
apply (transport_V (λx, right_inv f0 a ▸ x = h a) (left_inv (f1 _) _)),
apply apd
apply apdt
end
end pi

2
tests/lean/hott/531b.hlean
View file

@ -52,7 +52,7 @@ namespace colimit
definition comp_cglue [D : diagram] {P : colimit D → Type}
(Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
(Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▸ Pincl (hom j x) = Pincl x)
{j : Ihom} (x : ob (dom j)) : apd (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
{j : Ihom} (x : ob (dom j)) : apdt (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
--the sorry's in the statement can be removed when comp_incl is definitional
sorry --idp