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

various cleanup changes in library

Browse source 
some of the changes are backported from the hott3 library
pi_pathover and pi_pathover' are interchanged (same for variants and for sigma)
various definitions received explicit arguments: pinverse and eq_equiv_homotopy and ***.sigma_char
eq_of_fn_eq_fn is renamed to inj
in definitions about higher loop spaces and homotopy groups, the natural number arguments are now consistently before the type arguments
This commit is contained in:
Floris van Doorn 2018-09-07 16:30:58 +02:00
parent afdcf7cb71
commit 3d0d0947d6
45 changed files with 239 additions and 255 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -120,7 +120,7 @@ namespace category
(q : Πa b c g f, cast p (@comp ob C a b c g f) = @comp ob D a b c (cast p g) (cast p f))
: C = D :=
begin
apply eq_of_fn_eq_fn !category.sigma_char,
apply inj !category.sigma_char,
fapply sigma_eq,
{ induction C, induction D, esimp, exact precategory_eq @p q},
{ unfold is_univalent, apply is_prop.elimo},

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

@ -739,7 +739,7 @@ namespace functor
apply concat, apply assoc,
apply concat, apply ap (λ x, x ∘ _), apply X_phi_hom_of_eq, esimp[XF],
refine !respect_comp⁻¹ ⬝ ap (to_fun_hom F) _ ⬝ !respect_comp,
apply eq_of_fn_eq_fn' (to_fun_hom H),
apply inj' (to_fun_hom H),
refine !respect_comp ⬝ _ ⬝ !respect_comp⁻¹,
apply concat, apply ap (λ x, x ∘ _) !(right_inv (to_fun_hom H)),
apply concat, rotate 1, apply ap (λ x, _ ∘ x) !(right_inv (to_fun_hom H))⁻¹,

8
hott/algebra/category/functor/attributes.hlean
View file

@ -43,14 +43,14 @@ namespace category
definition hom_inv_respect_id (F : C ⇒ D) [H : fully_faithful F] (c : C) :
hom_inv F (ID (F c)) = id :=
begin
apply eq_of_fn_eq_fn' (to_fun_hom F),
apply inj' (to_fun_hom F),
exact !(right_inv (to_fun_hom F)) ⬝ !respect_id⁻¹,
end
definition hom_inv_respect_comp (F : C ⇒ D) [H : fully_faithful F] {a b c : C}
(g : F b ⟶ F c) (f : F a ⟶ F b) : hom_inv F (g ∘ f) = hom_inv F g ∘ hom_inv F f :=
begin
apply eq_of_fn_eq_fn' (to_fun_hom F),
apply inj' (to_fun_hom F),
refine !(right_inv (to_fun_hom F)) ⬝ _ ⬝ !respect_comp⁻¹,
rewrite [right_inv (to_fun_hom F), right_inv (to_fun_hom F)],
end
@ -60,9 +60,9 @@ namespace category
begin
fconstructor,
{ exact (to_fun_hom F)⁻¹ᶠ (F f)⁻¹},
{ apply eq_of_fn_eq_fn' (to_fun_hom F),
{ apply inj' (to_fun_hom F),
rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,left_inverse]},
{ apply eq_of_fn_eq_fn' (to_fun_hom F),
{ apply inj' (to_fun_hom F),
rewrite [respect_comp,right_inv (to_fun_hom F),respect_id,right_inverse]},
end

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

@ -161,7 +161,7 @@ namespace category
{ exact inverse_of_fully_faithful_of_split_essentially_surjective},
{ fapply natural_iso.mk',
{ intro c, esimp, apply reflect_iso F, exact (H₂ (F c)).2},
intro c c' f, esimp, apply eq_of_fn_eq_fn' (to_fun_hom F),
intro c c' f, esimp, apply inj' (to_fun_hom F),
rewrite [+respect_comp, +right_inv (to_fun_hom F), comp_inverse_cancel_left]},
{ fapply natural_iso.mk',
{ intro c, esimp, exact (H₂ c).2},

2
hott/algebra/group_theory.hlean
View file

@ -182,7 +182,7 @@ namespace group
definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ :=
homomorphism.mk φ⁻¹
abstract begin
intro g₁ g₂, apply eq_of_fn_eq_fn' φ,
intro g₁ g₂, apply inj' φ,
rewrite [respect_mul φ, +right_inv φ]
end end

62
hott/algebra/homotopy_group.hlean
View file

@ -10,8 +10,6 @@ import .trunc_group types.trunc .group_theory types.nat.hott
open nat eq pointed trunc is_trunc algebra group function equiv unit is_equiv nat
-- TODO: consistently make n an argument before A
-- TODO: rename homotopy_group_functor_compose to homotopy_group_functor_pcompose
namespace eq
definition inf_pgroup_loop [constructor] [instance] (A : Type*) : inf_pgroup (Ω A) :=
@ -103,7 +101,7 @@ namespace eq
π[k] (ptrunc k A) ≃* π[k] A :=
homotopy_group_ptrunc_of_le (le.refl k) A
theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πg[n+1] A ≃g G0 :=
theorem trivial_homotopy_of_is_set (n : ℕ) (A : Type*) [H : is_set A] : πg[n+1] A ≃g G0 :=
begin
apply trivial_group_of_is_contr,
apply is_trunc_trunc_of_is_trunc,
@ -111,30 +109,30 @@ namespace eq
apply is_trunc_succ_succ_of_is_set
end
definition homotopy_group_succ_out (A : Type*) (n : ℕ) : π[n + 1] A = π₁ (Ω[n] A) := idp
definition homotopy_group_succ_out (n : ℕ) (A : Type*) : π[n + 1] A = π₁ (Ω[n] A) := idp
definition homotopy_group_succ_in (A : Type*) (n : ℕ) : π[n + 1] A ≃* π[n] (Ω A) :=
ptrunc_pequiv_ptrunc 0 (loopn_succ_in A n)
definition homotopy_group_succ_in (n : ℕ) (A : Type*) : π[n + 1] A ≃* π[n] (Ω A) :=
ptrunc_pequiv_ptrunc 0 (loopn_succ_in n A)
definition ghomotopy_group_succ_out (A : Type*) (n : ℕ) : πg[n + 1] A = π₁ (Ω[n] A) := idp
definition ghomotopy_group_succ_out (n : ℕ) (A : Type*) : πg[n + 1] A = π₁ (Ω[n] A) := idp
definition homotopy_group_succ_in_con {A : Type*} {n : ℕ} (g h : πg[n + 2] A) :
homotopy_group_succ_in A (succ n) (g * h) =
homotopy_group_succ_in A (succ n) g * homotopy_group_succ_in A (succ n) h :=
definition homotopy_group_succ_in_con {n : ℕ} {A : Type*} (g h : πg[n + 2] A) :
homotopy_group_succ_in (succ n) A (g * h) =
homotopy_group_succ_in (succ n) A g * homotopy_group_succ_in (succ n) A h :=
begin
induction g with p, induction h with q, esimp,
apply ap tr, apply loopn_succ_in_con
end
definition ghomotopy_group_succ_in [constructor] (A : Type*) (n : ℕ) :
definition ghomotopy_group_succ_in [constructor] (n : ℕ) (A : Type*) :
πg[n + 2] A ≃g πg[n + 1] (Ω A) :=
begin
fapply isomorphism_of_equiv,
{ exact homotopy_group_succ_in A (succ n)},
{ exact homotopy_group_succ_in_con},
{ exact homotopy_group_succ_in (succ n) A },
{ exact homotopy_group_succ_in_con },
end
definition is_contr_homotopy_group_of_is_contr (A : Type*) (n : ℕ) [is_contr A] : is_contr (π[n] A) :=
definition is_contr_homotopy_group_of_is_contr (n : ℕ) (A : Type*) [is_contr A] : is_contr (π[n] A) :=
begin
apply is_trunc_trunc_of_is_trunc,
apply is_contr_loop_of_is_trunc,
@ -154,35 +152,35 @@ namespace eq
definition homotopy_group_functor_pid (n : ℕ) (A : Type*) : π→[n] (pid A) ~* pid (π[n] A) :=
ptrunc_functor_phomotopy 0 !apn_pid ⬝* !ptrunc_functor_pid
definition homotopy_group_functor_compose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
definition homotopy_group_functor_pcompose [constructor] (n : ℕ) {A B C : Type*} (g : B →* C)
(f : A →* B) : π→[n] (g ∘* f) ~* π→[n] g ∘* π→[n] f :=
ptrunc_functor_phomotopy 0 !apn_pcompose ⬝* !ptrunc_functor_pcompose
definition is_equiv_homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
[is_equiv f] : is_equiv (π→[n] f) :=
@(is_equiv_trunc_functor 0 _) !is_equiv_apn
(H : is_equiv f) : is_equiv (π→[n] f) :=
@(is_equiv_trunc_functor 0 _) (is_equiv_apn n f H)
definition homotopy_group_succ_in_natural (n : ℕ) {A B : Type*} (f : A →* B) :
homotopy_group_succ_in B n ∘* π→[n + 1] f ~*
π→[n] (Ω→ f) ∘* homotopy_group_succ_in A n :=
homotopy_group_succ_in n B ∘* π→[n + 1] f ~*
π→[n] (Ω→ f) ∘* homotopy_group_succ_in n A :=
begin
refine !ptrunc_functor_pcompose⁻¹* ⬝* _ ⬝* !ptrunc_functor_pcompose,
exact ptrunc_functor_phomotopy 0 (apn_succ_phomotopy_in n f)
end
definition homotopy_group_succ_in_natural_unpointed (n : ℕ) {A B : Type*} (f : A →* B) :
hsquare (homotopy_group_succ_in A n) (homotopy_group_succ_in B n) (π→[n+1] f) (π→[n] (Ω→ f)) :=
hsquare (homotopy_group_succ_in n A) (homotopy_group_succ_in n B) (π→[n+1] f) (π→[n] (Ω→ f)) :=
(homotopy_group_succ_in_natural n f)⁻¹*
definition is_equiv_homotopy_group_functor_ap1 (n : ℕ) {A B : Type*} (f : A →* B)
[is_equiv (π→[n + 1] f)] : is_equiv (π→[n] (Ω→ f)) :=
have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in A n),
from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in B n)
have is_equiv (π→[n] (Ω→ f) ∘ homotopy_group_succ_in n A),
from is_equiv_of_equiv_of_homotopy (equiv.mk (π→[n+1] f) _ ⬝e homotopy_group_succ_in n B)
(homotopy_group_succ_in_natural n f),
is_equiv.cancel_right (homotopy_group_succ_in A n) _
is_equiv.cancel_right (homotopy_group_succ_in n A) _
definition tinverse [constructor] {X : Type*} : π[1] X →* π[1] X :=
ptrunc_functor 0 pinverse
ptrunc_functor 0 (pinverse X)
definition is_equiv_tinverse [constructor] (A : Type*) : is_equiv (@tinverse A) :=
by apply @is_equiv_trunc_functor; apply is_equiv_eq_inverse
@ -218,14 +216,14 @@ namespace eq
definition homotopy_group_homomorphism_pcompose (n : ℕ) [H : is_succ n] {A B C : Type*} (g : B →* C)
(f : A →* B) : π→g[n] (g ∘* f) ~ π→g[n] g ∘ π→g[n] f :=
begin
induction H with n, exact to_homotopy (homotopy_group_functor_compose (succ n) g f)
induction H with n, exact to_homotopy (homotopy_group_functor_pcompose (succ n) g f)
end
definition homotopy_group_isomorphism_of_pequiv [constructor] (n : ℕ) {A B : Type*} (f : A ≃* B)
: πg[n+1] A ≃g πg[n+1] B :=
begin
apply isomorphism.mk (homotopy_group_homomorphism (succ n) f),
esimp, apply is_equiv_trunc_functor, apply is_equiv_apn,
exact is_equiv_homotopy_group_functor _ _ _,
end
definition homotopy_group_add (A : Type*) (n m : ℕ) :
@ -238,11 +236,11 @@ namespace eq
exact !loopn_succ_in⁻¹ᵉ*}
end
theorem trivial_homotopy_add_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ)
theorem trivial_homotopy_add_of_is_set_loopn {n : ℕ} (m : ℕ) {A : Type*}
(H : is_set (Ω[n] A)) : πg[m+n+1] A ≃g G0 :=
!homotopy_group_add ⬝g !trivial_homotopy_of_is_set
theorem trivial_homotopy_le_of_is_set_loopn {A : Type*} {n : ℕ} (m : ℕ) (H1 : n ≤ m)
theorem trivial_homotopy_le_of_is_set_loopn {n : ℕ} (m : ℕ) (H1 : n ≤ m) {A : Type*}
(H2 : is_set (Ω[n] A)) : πg[m+1] A ≃g G0 :=
obtain (k : ℕ) (p : n + k = m), from le.elim H1,
isomorphism_of_eq (ap (λx, πg[x+1] A) (p⁻¹ ⬝ add.comm n k)) ⬝g
@ -300,8 +298,8 @@ namespace eq
definition homotopy_group_functor_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) :
psquare (π→[n] f₁₀) (π→[n] f₁₂) (π→[n] f₀₁) (π→[n] f₂₁) :=
!homotopy_group_functor_compose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
!homotopy_group_functor_compose
!homotopy_group_functor_pcompose⁻¹* ⬝* homotopy_group_functor_phomotopy n p ⬝*
!homotopy_group_functor_pcompose
definition homotopy_group_homomorphism_psquare (n : ℕ) [H : is_succ n]
(p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : hsquare (π→g[n] f₁₀) (π→g[n] f₁₂) (π→g[n] f₀₁) (π→g[n] f₂₁) :=
@ -313,7 +311,7 @@ namespace eq
/- some homomorphisms -/
-- definition is_homomorphism_cast_loopn_succ_eq_in {A : Type*} (n : ℕ) :
-- definition is_homomorphism_cast_loopn_succ_eq_in (n : ℕ) {A : Type*} :
-- is_homomorphism (loopn_succ_in A (succ n) : πg[n+1+1] A → πg[n+1] (Ω A)) :=
-- begin
-- intro g h, induction g with g, induction h with h,
@ -321,7 +319,7 @@ namespace eq
-- loopn_succ_eq_in_concat, - + tr_compose],
-- end
definition is_mul_hom_inverse (A : Type*) (n : ℕ)
definition is_mul_hom_inverse (n : ℕ) (A : Type*)
: is_mul_hom (λp, p⁻¹ : (πag[n+2] A) → (πag[n+2] A)) :=
begin
intro g h, exact ap inv (mul.comm g h) ⬝ mul_inv h g,

2
hott/cubical/square.hlean
View file

@ -668,7 +668,7 @@ namespace eq
induction r₁₀, induction r₀₁, induction r₁₂, induction r₂₁,
induction p₁₂, induction p₁₀, induction p₂₁, esimp at *, induction s₁₁, esimp at *,
esimp [square_of_eq],
apply eq_of_fn_eq_fn !square_equiv_eq, esimp,
apply inj !square_equiv_eq, esimp,
exact (eq_bot_of_square u)⁻¹
end

2
hott/cubical/squareover.hlean
View file

@ -242,7 +242,7 @@ namespace eq
induction p₁₀, -- if needed we can remove this induction and use con_tr_idp in types/eq2
rewrite [▸* at H,idp_con at H,+ap_id at H],
let H' := eq_of_vdeg_square H,
exact eq_of_fn_eq_fn !pathover_equiv_tr_eq H'
exact inj !pathover_equiv_tr_eq H'
end
-- definition vdeg_tr_squareover {q₁₂ : p₀₁ ▸ b₀₀ =[p₁₂] p₂₁ ▸ b₂₀} (r : q₁₀ =[_] q₁₂)

12
hott/eq2.hlean
View file

@ -248,7 +248,7 @@ namespace eq
(H : P (idpath (f a₀))) ⦃a₁ : A⦄ (p : f a₀ = f a₁) : P p :=
begin
assert qr : Σ(q : a₀ = a₁), ap f q = p,
{ exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
{ exact ⟨inj f p, ap_inj' f p⟩ },
cases qr with q r, apply transport P r, induction q, exact H
end
@ -256,7 +256,7 @@ namespace eq
(H : P (idpath (f a₁))) ⦃a₀ : A⦄ (p : f a₀ = f a₁) : P p :=
begin
assert qr : Σ(q : a₀ = a₁), ap f q = p,
{ exact ⟨eq_of_fn_eq_fn f p, ap_eq_of_fn_eq_fn' f p⟩ },
{ exact ⟨inj f p, ap_inj' f p⟩ },
cases qr with q r, apply transport P r, induction q, exact H
end
@ -273,11 +273,11 @@ namespace eq
⦃a₁' : A'⦄ (p' : f a₀ = g a₁') (H : P p') ⦃a₁ : A'⦄ (p : f a₀ = g a₁) : P p :=
begin
assert qr : Σ(q : g⁻¹ (f a₀) = a₁), (right_inv g (f a₀))⁻¹ ⬝ ap g q = p,
{ exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p),
whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
{ exact ⟨inj g (right_inv g (f a₀) ⬝ p),
whisker_left _ (ap_inj' g _) ⬝ !inv_con_cancel_left⟩ },
assert q'r' : Σ(q' : g⁻¹ (f a₀) = a₁'), (right_inv g (f a₀))⁻¹ ⬝ ap g q' = p',
{ exact ⟨eq_of_fn_eq_fn g (right_inv g (f a₀) ⬝ p'),
whisker_left _ (ap_eq_of_fn_eq_fn' g _) ⬝ !inv_con_cancel_left⟩ },
{ exact ⟨inj g (right_inv g (f a₀) ⬝ p'),
whisker_left _ (ap_inj' g _) ⬝ !inv_con_cancel_left⟩ },
induction qr with q r, induction q'r' with q' r',
induction q, induction q',
induction r, induction r',

2
hott/hit/coeq.hlean
View file

@ -58,7 +58,7 @@ 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 eq_of_fn_eq_fn_inv !(pathover_constant (cp x)),
apply inj_inv !(pathover_constant (cp x)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cp],
end

4
hott/hit/colimit.hlean
View file

@ -67,7 +67,7 @@ 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 eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)),
apply inj_inv !(pathover_constant (cglue j x)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cglue],
end
@ -157,7 +157,7 @@ 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 eq_of_fn_eq_fn_inv !(pathover_constant (glue a)),
apply inj_inv !(pathover_constant (glue a)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_glue],
end

2
hott/hit/groupoid_quotient.hlean
View file

@ -219,7 +219,7 @@ section
definition encode_con (p : elt a = elt b)
(q : elt b = elt c) : encode (elt c) (p ⬝ q) = encode (elt c) q ∘ encode (elt b) p :=
begin
apply eq_of_fn_eq_fn (elt_eq_elt_equiv a c)⁻¹ᵉ,
apply inj (elt_eq_elt_equiv a c)⁻¹ᵉ,
refine !right_inv ⬝ _ ⬝ !decode_comp⁻¹,
apply concat2, do 2 exact (to_left_inv !elt_eq_elt_equiv _)⁻¹
end

2
hott/hit/prop_trunc.hlean
View file

@ -78,7 +78,7 @@ namespace one_step_tr
(Pe : Π(a a' : A), Pt a = Pt a') (a a' : A)
: 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')),
apply inj_inv !(pathover_constant (tr_eq a a')),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq],
end

2
hott/hit/pushout.hlean
View file

@ -66,7 +66,7 @@ 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 eq_of_fn_eq_fn_inv !(pathover_constant (glue x)),
apply inj_inv !(pathover_constant (glue x)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue],
end

4
hott/hit/quotient.hlean
View file

@ -34,7 +34,7 @@ namespace quotient
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
: 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)),
apply inj_inv !(pathover_constant (eq_of_rel R H)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel],
end
@ -148,7 +148,7 @@ namespace quotient
induction v with q p,
induction q,
{ exact Qpt p},
{ apply pi_pathover_left', esimp, intro c,
{ apply pi_pathover_left, esimp, intro c,
refine _ ⬝op apdt Qpt (elim_type_eq_of_rel C f H c)⁻¹ᵖ,
refine _ ⬝op (tr_compose Q Ppt _ _)⁻¹ ,
rewrite ap_inv,

2
hott/hit/set_quotient.hlean
View file

@ -59,7 +59,7 @@ section
(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 eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)),
apply inj_inv !(pathover_constant (eq_of_rel H)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel],
end

4
hott/hit/trunc.hlean
View file

@ -71,7 +71,7 @@ namespace trunc
exact fn_tr_eq_tr_fn p (λy, tr) x ⬝ !tr_compose
end
definition is_equiv_trunc_functor [constructor] (f : X → Y) [H : is_equiv f]
definition is_equiv_trunc_functor [constructor] (f : X → Y) (H : is_equiv f)
: is_equiv (trunc_functor n f) :=
adjointify _
(trunc_functor n f⁻¹)
@ -83,7 +83,7 @@ namespace trunc
section
definition trunc_equiv_trunc [constructor] (f : X ≃ Y) : trunc n X ≃ trunc n Y :=
equiv.mk _ (is_equiv_trunc_functor n f)
equiv.mk _ (is_equiv_trunc_functor n f _)
end
section

2
hott/hit/two_quotient.hlean
View file

@ -92,7 +92,7 @@ namespace simple_two_quotient
(Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a = Pj a') ⦃a a' : A⦄ (s : R a a')
: ap (pre_elim Pj Pa Pe) (e s) = Pe s :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)),
apply inj_inv !(pathover_constant (e s)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pre_elim,rec_e],
end

2
hott/homotopy/EM.hlean
View file

@ -257,7 +257,7 @@ namespace EM
{ rewrite [EMadd1_succ G (succ n)],
refine (ptrunc_pequiv (succ n + 1) _)⁻¹ᵉ* ⬝e* _ ⬝e* (loop_ptrunc_pequiv _ _)⁻¹ᵉ*,
have succ n + 1 ≤ 2 * succ n, from add_mul_le_mul_add n 1 1,
refine freudenthal_pequiv _ this }
refine freudenthal_pequiv this _ }
end
definition loopn_EMadd1_pequiv_EM1 (G : AbGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) :=

24
hott/homotopy/LES_of_homotopy_groups.hlean
View file

@ -181,7 +181,7 @@ namespace chain_complex
(fiber_sequence_carrier_pequiv n ∘*
fiber_sequence_fun (n + 3)) ∘*
(fiber_sequence_carrier_pequiv (n + 1))⁻¹ᵉ* ~*
Ω→ (fiber_sequence_fun n) ∘* pinverse :=
Ω→ (fiber_sequence_fun n) ∘* !pinverse :=
begin
fapply phomotopy.mk,
{ exact chain_complex.fiber_sequence_fun_eq_helper f n},
@ -203,7 +203,7 @@ namespace chain_complex
theorem fiber_sequence_fun_phomotopy (n : ℕ) :
fiber_sequence_carrier_pequiv n ∘*
fiber_sequence_fun (n + 3) ~*
(Ω→ (fiber_sequence_fun n) ∘* pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
(Ω→ (fiber_sequence_fun n) ∘* !pinverse) ∘* fiber_sequence_carrier_pequiv (n + 1) :=
begin
apply phomotopy_of_pinv_right_phomotopy,
apply fiber_sequence_fun_phomotopy_helper
@ -271,7 +271,7 @@ namespace chain_complex
by reflexivity
definition pid_or_pinverse_add4_rev (n : ℕ) :
pid_or_pinverse (n + 4) ~* pinverse ∘* Ω→(pid_or_pinverse (n + 1)) :=
pid_or_pinverse (n + 4) ~* !pinverse ∘* Ω→(pid_or_pinverse (n + 1)) :=
!ap1_pcompose_pinverse
theorem fiber_sequence_phomotopy_loop_spaces : Π(n : ℕ),
@ -312,7 +312,7 @@ namespace chain_complex
| 0 := !pid
| 1 := !pid
| 2 := !pid
| (k+3) := Ω→(pid_or_pinverse_right k) ∘* pinverse
| (k+3) := Ω→(pid_or_pinverse_right k) ∘* !pinverse
definition pid_or_pinverse_left : Π(n : ℕ), loop_spaces n →* loop_spaces n
| 0 := pequiv.rfl
@ -320,14 +320,14 @@ namespace chain_complex
| 2 := pequiv.rfl
| 3 := pequiv.rfl
| 4 := pequiv.rfl
| (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* pinverse
| (k+5) := Ω→(pid_or_pinverse_left (k+2)) ∘* !pinverse
definition pid_or_pinverse_right_add3 (n : ℕ)
: pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* pinverse :=
: pid_or_pinverse_right (n + 3) = Ω→(pid_or_pinverse_right n) ∘* !pinverse :=
by reflexivity
definition pid_or_pinverse_left_add5 (n : ℕ)
: pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* pinverse :=
: pid_or_pinverse_left (n + 5) = Ω→(pid_or_pinverse_left (n+2)) ∘* !pinverse :=
by reflexivity
theorem pid_or_pinverse_commute_right : Π(n : ℕ),
@ -420,7 +420,7 @@ namespace chain_complex
definition loop_spaces_fun2 : Π(n : +3ℕ), loop_spaces2 (S n) →* loop_spaces2 n
| (n, fin.mk 0 H) := proof Ω→[n] f qed
| (n, fin.mk 1 H) := proof Ω→[n] (ppoint f) qed
| (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in Y n qed
| (n, fin.mk 2 H) := proof Ω→[n] boundary_map ∘* loopn_succ_in n Y qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition loop_spaces_fun2_add1_0 (n : ℕ) (H : 0 < succ 2)
@ -580,7 +580,7 @@ namespace chain_complex
| (n, fin.mk 0 H) := proof π→[n] f qed
| (n, fin.mk 1 H) := proof π→[n] (ppoint f) qed
| (n, fin.mk 2 H) :=
proof π→[n] boundary_map ∘* homotopy_group_succ_in Y n qed
proof π→[n] boundary_map ∘* homotopy_group_succ_in n Y qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition homotopy_groups_fun_phomotopy_loop_spaces_fun2 [reducible]
@ -638,7 +638,7 @@ namespace chain_complex
cc_to_fn LES_of_homotopy_groups (n, 1) = π→[n] (ppoint f) :=
by reflexivity
definition LES_of_homotopy_groups_fun_2 : cc_to_fn LES_of_homotopy_groups (n, 2) =
π→[n] boundary_map ∘* homotopy_group_succ_in Y n :=
π→[n] boundary_map ∘* homotopy_group_succ_in n Y :=
by reflexivity
open group
@ -673,7 +673,7 @@ namespace chain_complex
begin
apply homomorphism.mk (cc_to_fn LES_of_homotopy_groups (k + 1, 2)),
exact abstract begin rewrite [LES_of_homotopy_groups_fun_2],
refine homomorphism.struct ((π→g[k+1] boundary_map) ∘g ghomotopy_group_succ_in Y k),
refine homomorphism.struct ((π→g[k+1] boundary_map) ∘g ghomotopy_group_succ_in k Y),
end end
end
| (k, fin.mk (l+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
@ -749,7 +749,7 @@ namespace chain_complex
: Π(n : +3ℕ), fibration_sequence_car (S n) →* fibration_sequence_car n
| (n, fin.mk 0 H) := proof Ω→[n] f qed
| (n, fin.mk 1 H) := proof Ω→[n] g qed
| (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in Y n qed
| (n, fin.mk 2 H) := proof Ω→[n] (e ∘* boundary_map f) ∘* loopn_succ_in n Y qed
| (n, fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition fibration_sequence_pequiv : Π(x : +3ℕ),

14
hott/homotopy/circle.hlean
View file

@ -59,14 +59,14 @@ 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 eq_of_fn_eq_fn_inv !(pathover_constant seg1),
apply inj_inv !(pathover_constant 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),
apply inj_inv !(pathover_constant seg2),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg2],
end
@ -122,14 +122,14 @@ namespace circle
theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
ap (circle.elim Pbase Ploop) loop = Ploop :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant loop),
apply inj_inv !(pathover_constant 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),
apply inj_inv !(pathover_constant seg1),
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
@ -138,7 +138,7 @@ namespace circle
theorem elim_seg2 {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
: ap (circle.elim Pbase Ploop) seg2 = Ploop ⬝ (tr_constant seg1 Pbase)⁻¹ :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant seg2),
apply inj_inv !(pathover_constant seg2),
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₂)
@ -295,7 +295,7 @@ namespace circle
trunc_equiv_trunc 0 base_eq_base_equiv ⬝e @(trunc_equiv 0 ℤ) proof _ qed
definition con_comm_base (p q : base = base) : p ⬝ q = q ⬝ p :=
eq_of_fn_eq_fn base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
inj base_eq_base_equiv (by esimp;rewrite [+encode_con,add.comm])
definition fundamental_group_of_circle : π₁(S¹*) ≃g gℤ :=
begin
@ -308,7 +308,7 @@ namespace circle
open nat
definition homotopy_group_of_circle (n : ℕ) : πg[n+2] S¹* ≃g G0 :=
begin
refine @trivial_homotopy_add_of_is_set_loopn S¹* 1 n _,
refine @trivial_homotopy_add_of_is_set_loopn 1 n S¹* _,
exact is_trunc_equiv_closed_rev _ base_eq_base_equiv _
end

8
hott/homotopy/connectedness.hlean
View file

@ -97,11 +97,11 @@ namespace is_conn
rewrite [-(ap (λv a, v (f a)) (apd10_eq_of_homotopy_fn r))],
rewrite [-(apd10_ap_precompose_dependent f (eq_of_homotopy r))],
apply equiv.symm,
apply eq_equiv_fn_eq (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a)))
apply eq_equiv_fn_eq_of_is_equiv (@apd10 A (λa, P (f a)) (λa, g (f a)) (λa, h (f a)))
end,
apply equiv.trans (sigma.sigma_equiv_sigma_right e'), clear e',
apply equiv.trans (equiv.symm (sigma.sigma_equiv_sigma_left
eq_equiv_homotopy)),
!eq_equiv_homotopy)),
apply equiv.symm, apply equiv.trans !fiber_eq_equiv,
apply sigma.sigma_equiv_sigma_right, intro r,
apply eq_equiv_eq_symm
@ -321,7 +321,7 @@ namespace is_conn
[H2 : is_conn_fun k f] : is_conn_fun k (trunc_functor n f) :=
begin
apply is_conn_fun_of_is_equiv,
apply is_equiv_trunc_functor_of_le f H
exact is_equiv_trunc_functor_of_le f H _
end
-- Exercise 7.18
@ -427,7 +427,7 @@ namespace is_conn
begin
apply is_conn_fun_of_is_equiv,
have H3 : is_equiv (trunc_functor k f), from !is_equiv_trunc_functor_of_is_conn_fun,
have H4 : is_equiv (trunc_functor n f), from is_equiv_trunc_functor_of_le _ H,
have H4 : is_equiv (trunc_functor n f), from is_equiv_trunc_functor_of_le _ H _,
apply is_equiv_of_equiv_of_homotopy (equiv.mk (trunc_functor n f) _ ⬝e !trunc_equiv),
intro x, induction x, reflexivity
end

2
hott/homotopy/cylinder.hlean
View file

@ -67,7 +67,7 @@ section
(Pseg : Π(a : A), Pbase (f a) = Ptop a)
(a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)),
apply inj_inv !(pathover_constant (seg a)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_seg],
end

56
hott/homotopy/freudenthal.hlean
View file

@ -167,29 +167,29 @@ namespace freudenthal section
end end freudenthal
open algebra group
definition freudenthal_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
definition freudenthal_pequiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A]
: ptrunc k A ≃* ptrunc k (Ω (susp A)) :=
have H' : k ≤[ℕ₋₂] n + n,
by rewrite [mul.comm at H, -algebra.zero_add n at {1}]; exact of_nat_le_of_nat H,
ptrunc_pequiv_ptrunc_of_le H' (freudenthal.pequiv' A n)
definition freudenthal_equiv {A : Type*} {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
definition freudenthal_equiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A]
: trunc k A ≃ trunc k (Ω (susp A)) :=
freudenthal_pequiv A H
freudenthal_pequiv H A
definition freudenthal_homotopy_group_pequiv (A : Type*) {n k : ℕ} [is_conn n A] (H : k ≤ 2 * n)
definition freudenthal_homotopy_group_pequiv {n k : ℕ} (H : k ≤ 2 * n) (A : Type*) [is_conn n A]
: π[k + 1] (susp A) ≃* π[k] A :=
calc
π[k + 1] (susp A) ≃* π[k] (Ω (susp A)) : homotopy_group_succ_in (susp A) k
π[k + 1] (susp A) ≃* π[k] (Ω (susp A)) : homotopy_group_succ_in k (susp A)
... ≃* Ω[k] (ptrunc k (Ω (susp A))) : homotopy_group_pequiv_loop_ptrunc k (Ω (susp A))
... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv A H)
... ≃* Ω[k] (ptrunc k A) : loopn_pequiv_loopn k (freudenthal_pequiv H A)
... ≃* π[k] A : (homotopy_group_pequiv_loop_ptrunc k A)⁻¹ᵉ*
definition freudenthal_homotopy_group_isomorphism (A : Type*) {n k : ℕ} [is_conn n A]
(H : k + 1 ≤ 2 * n) : πg[k+2] (susp A) ≃g πg[k + 1] A :=
definition freudenthal_homotopy_group_isomorphism {n k : ℕ} (H : k + 1 ≤ 2 * n)
(A : Type*) [is_conn n A] : πg[k+2] (susp A) ≃g πg[k + 1] A :=
begin
fapply isomorphism_of_equiv,
{ exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv A H)},
{ exact equiv_of_pequiv (freudenthal_homotopy_group_pequiv H A)},
{ intro g h,
refine _ ⬝ !homotopy_group_pequiv_loop_ptrunc_inv_con,
apply ap !homotopy_group_pequiv_loop_ptrunc⁻¹ᵉ*,
@ -198,17 +198,17 @@ begin
apply homotopy_group_succ_in_con}
end
definition to_pmap_freudenthal_pequiv {A : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n)
: freudenthal_pequiv A H ~* ptrunc_functor k (loop_susp_unit A) :=
definition to_pmap_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) (A : Type*) [is_conn n A]
: freudenthal_pequiv H A ~* ptrunc_functor k (loop_susp_unit A) :=
begin
fapply phomotopy.mk,
{ intro x, induction x with a, reflexivity },
{ refine !idp_con ⬝ _, refine _ ⬝ ap02 _ !idp_con⁻¹, refine _ ⬝ !ap_compose, apply ap_compose }
end
definition ptrunc_elim_freudenthal_pequiv {A B : Type*} (n k : ℕ) [is_conn n A] (H : k ≤ 2 * n)
definition ptrunc_elim_freudenthal_pequiv (n k : ℕ) (H : k ≤ 2 * n) {A B : Type*} [is_conn n A]
(f : A →* Ω B) [is_trunc (k.+1) (B)] :
ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv A H ~* ptrunc.elim k f :=
ptrunc.elim k (Ω→ (susp_elim f)) ∘* freudenthal_pequiv H A ~* ptrunc.elim k f :=
begin
refine pwhisker_left _ !to_pmap_freudenthal_pequiv ⬝* _,
refine !ptrunc_elim_ptrunc_functor ⬝* _,
@ -220,12 +220,12 @@ namespace susp
definition iterate_susp_stability_pequiv_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A]
(H : k ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) :=
have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _,
freudenthal_homotopy_group_pequiv (iterate_susp n A) H
freudenthal_homotopy_group_pequiv H (iterate_susp n A)
definition iterate_susp_stability_isomorphism_of_is_conn_0 (A : Type*) {k n : ℕ} [is_conn 0 A]
(H : k + 1 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) :=
definition iterate_susp_stability_isomorphism_of_is_conn_0 {k n : ℕ} (H : k + 1 ≤ 2 * n)
(A : Type*) [is_conn 0 A] : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) :=
have is_conn n (iterate_susp n A), by rewrite [-zero_add n]; exact _,
freudenthal_homotopy_group_isomorphism (iterate_susp n A) H
freudenthal_homotopy_group_isomorphism H (iterate_susp n A)
definition stability_helper1 {k n : ℕ} (H : k + 2 ≤ 2 * n) : k ≤ 2 * pred n :=
begin
@ -233,7 +233,7 @@ namespace susp
apply pred_le_pred, apply pred_le_pred, exact H
end
definition stability_helper2 (A : Type*) {k n : ℕ} (H : k + 2 ≤ 2 * n) :
definition stability_helper2 {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) :
is_conn (pred n) (iterate_susp n A) :=
have Π(n : ℕ), n = -1 + (n + 1),
begin intro n, induction n with n IH, reflexivity, exact ap succ IH end,
@ -243,17 +243,17 @@ namespace susp
{ esimp, rewrite [this n], exact is_conn_iterate_susp -1 _ A }
end
definition iterate_susp_stability_pequiv (A : Type*) {k n : ℕ}
(H : k + 2 ≤ 2 * n) : π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) :=
have is_conn (pred n) (iterate_susp n A), from stability_helper2 A H,
freudenthal_homotopy_group_pequiv (iterate_susp n A) (stability_helper1 H)
definition iterate_susp_stability_pequiv {k n : ℕ} (H : k + 2 ≤ 2 * n) (A : Type*) :
π[k + 1] (iterate_susp (n + 1) A) ≃* π[k] (iterate_susp n A) :=
have is_conn (pred n) (iterate_susp n A), from stability_helper2 H A,
freudenthal_homotopy_group_pequiv (stability_helper1 H) (iterate_susp n A)
definition iterate_susp_stability_isomorphism (A : Type*) {k n : ℕ}
(H : k + 3 ≤ 2 * n) : πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) :=
have is_conn (pred n) (iterate_susp n A), from @stability_helper2 A (k+1) n H,
freudenthal_homotopy_group_isomorphism (iterate_susp n A) (stability_helper1 H)
definition iterate_susp_stability_isomorphism {k n : ℕ} (H : k + 3 ≤ 2 * n) (A : Type*) :
πg[k+2] (iterate_susp (n + 1) A) ≃g πg[k+1] (iterate_susp n A) :=
have is_conn (pred n) (iterate_susp n A), from @stability_helper2 (k+1) n H A,
freudenthal_homotopy_group_isomorphism (stability_helper1 H) (iterate_susp n A)
definition iterated_freudenthal_pequiv (A : Type*) {n k m : ℕ} [HA : is_conn n A] (H : k ≤ 2 * n)
definition iterated_freudenthal_pequiv {n k m : ℕ} (H : k ≤ 2 * n) (A : Type*) [HA : is_conn n A]
: ptrunc k A ≃* ptrunc k (Ω[m] (iterate_susp m A)) :=
begin
revert A n k HA H, induction m with m IH: intro A n k HA H,
@ -263,7 +263,7 @@ namespace susp
succ k ≤ succ (2 * n) : succ_le_succ H
... ≤ 2 * succ n : self_le_succ,
exact calc
ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv A H
ptrunc k A ≃* ptrunc k (Ω (susp A)) : freudenthal_pequiv H A
... ≃* Ω (ptrunc (succ k) (susp A)) : loop_ptrunc_pequiv
... ≃* Ω (ptrunc (succ k) (Ω[m] (iterate_susp m (susp A)))) :
loop_pequiv_loop (IH (susp A) (succ n) (succ k) _ H2)

14
hott/homotopy/homotopy_group.hlean
View file

@ -79,8 +79,8 @@ namespace is_trunc
begin
have π→[k] pdown.{v u} ∘* π→[k] (plift_functor f) ∘* π→[k] pup.{u v} ~* π→[k] f,
begin
refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _,
refine !homotopy_group_functor_compose⁻¹* ⬝* _,
refine pwhisker_left _ !homotopy_group_functor_pcompose⁻¹* ⬝* _,
refine !homotopy_group_functor_pcompose⁻¹* ⬝* _,
apply homotopy_group_functor_phomotopy, apply plift_functor_phomotopy
end,
have π→[k] pdown.{v u} ∘ π→[k] (plift_functor f) ∘ π→[k] pup.{u v} ~ π→[k] f, from this,
@ -133,10 +133,10 @@ namespace is_trunc
pmap.to_fun (π→[k + 1] (pmap_of_map (ap f) p))),
begin
apply is_equiv_compose, exact this a p,
apply is_equiv_trunc_functor
exact is_equiv_trunc_functor _ _ _
end,
apply is_equiv.homotopy_closed, exact this,
refine !homotopy_group_functor_compose⁻¹* ⬝* _,
refine !homotopy_group_functor_pcompose⁻¹* ⬝* _,
apply homotopy_group_functor_phomotopy,
fapply phomotopy.mk,
{ esimp, intro q, refine !idp_con⁻¹},
@ -157,12 +157,12 @@ namespace is_trunc
apply is_equiv_compose
(π→[k + 1] (pointed_eta_pequiv B ⬝e* (pequiv_of_eq_pt (respect_pt f))⁻¹ᵉ*)),
apply is_equiv_compose (π→[k + 1] f),
all_goals apply is_equiv_homotopy_group_functor,
all_goals exact is_equiv_homotopy_group_functor _ _ _,
end,
refine @(is_equiv.homotopy_closed _) _ this _,
apply to_homotopy,
refine pwhisker_left _ !homotopy_group_functor_compose⁻¹* ⬝* _,
refine !homotopy_group_functor_compose⁻¹* ⬝* _,
refine pwhisker_left _ !homotopy_group_functor_pcompose⁻¹* ⬝* _,
refine !homotopy_group_functor_pcompose⁻¹* ⬝* _,
apply homotopy_group_functor_phomotopy, apply phomotopy_pmap_of_map
end

2
hott/homotopy/interval.hlean
View file

@ -44,7 +44,7 @@ namespace interval
theorem elim_seg {P : Type} (P0 P1 : P) (Ps : P0 = P1)
: ap (interval.elim P0 P1 Ps) seg = Ps :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant seg),
apply inj_inv !(pathover_constant seg),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑interval.elim,rec_seg],
end

2
hott/homotopy/join.hlean
View file

@ -45,7 +45,7 @@ namespace join
(Pglue : Π(x : A)(y : B), Pinl x = Pinr y) (x : A) (y : B)
: 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)),
apply equiv.inj_inv !(pathover_constant (glue x y)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑join.elim],
apply join.rec_glue
end

4
hott/homotopy/smash.hlean
View file

@ -109,7 +109,7 @@ namespace smash
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (a : A) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluel a) = Pgl a :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluel A B a)),
apply inj_inv !(pathover_constant (@gluel A B a)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluel],
end
@ -117,7 +117,7 @@ namespace smash
(Pgl : Πa : A, Pmk a pt = Pl) (Pgr : Πb : B, Pmk pt b = Pr) (b : B) :
ap (smash.elim Pmk Pl Pr Pgl Pgr) (gluer b) = Pgr b :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (@gluer A B b)),
apply inj_inv !(pathover_constant (@gluer A B b)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑smash.elim,rec_gluer],
end

2
hott/homotopy/sphere.hlean
View file

@ -38,7 +38,7 @@ namespace sphere
begin
induction n with n s,
{ exact tt },
{ exact (loopn_succ_in (S (succ n)) n)⁻¹ᵉ* (apn n (equator n) s) }
{ exact (loopn_succ_in n (S (succ n)))⁻¹ᵉ* (apn n (equator n) s) }
end
definition sphere_equiv_bool [constructor] : S 0 ≃ bool := by reflexivity

4
hott/homotopy/sphere2.hlean
View file

@ -56,11 +56,11 @@ namespace sphere
definition sphere_stability_pequiv (k n : ℕ) (H : k + 2 ≤ 2 * n) :
π[k + 1] (S (n+1)) ≃* π[k] (S n) :=
iterate_susp_stability_pequiv pbool H
iterate_susp_stability_pequiv H pbool
definition stability_isomorphism (k n : ℕ) (H : k + 3 ≤ 2 * n)
: πg[k+1 +1] (S (n+1)) ≃g πg[k+1] (S n) :=
iterate_susp_stability_isomorphism pbool H
iterate_susp_stability_isomorphism H pbool
open int circle hopf
definition πnSn (n : ℕ) [H : is_succ n] : πg[n] (S (n)) ≃g gℤ :=

4
hott/homotopy/susp.hlean
View file

@ -69,7 +69,7 @@ namespace susp
theorem elim_merid {P : Type} {PN PS : P} (Pm : A → PN = PS) (a : A)
: ap (susp.elim PN PS Pm) (merid a) = Pm a :=
begin
apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)),
apply inj_inv !(pathover_constant (merid a)),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑susp.elim,rec_merid],
end
@ -512,7 +512,7 @@ namespace susp
begin
revert X Y, induction n with n IH: intro X Y,
{ reflexivity },
{ refine !susp_adjoint_loop ⬝e* !IH ⬝e* _, apply pequiv_ppcompose_left,
{ refine !susp_adjoint_loop ⬝e* !IH ⬝e* _, apply ppmap_pequiv_ppmap_right,
symmetry, apply loopn_succ_in }
end

39
hott/init/equiv.hlean
View file

@ -174,10 +174,10 @@ namespace is_equiv
have Hfinv : is_equiv f⁻¹, from is_equiv_inv f,
@homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (f ∘ g)) (λa, left_inv f (g a))
definition eq_of_fn_eq_fn' [unfold 4] {x y : A} (q : f x = f y) : x = y :=
definition inj' [unfold 4] {x y : A} (q : f x = f y) : x = y :=
(left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
definition ap_inj' {x y : A} (q : f x = f y) : ap f (inj' f q) = q :=
!ap_con ⬝ whisker_right _ !ap_con
⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
◾ (inverse (ap_compose f f⁻¹ _))
@ -186,15 +186,15 @@ namespace is_equiv
⬝ whisker_right _ !con.left_inv
⬝ !idp_con
definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q :=
definition inj'_ap {x y : A} (q : x = y) : inj' f (ap f q) = q :=
by induction q; apply con.left_inv
definition is_equiv_ap [instance] [constructor] (x y : A) : is_equiv (ap f : x = y → f x = f y) :=
adjointify
(ap f)
(eq_of_fn_eq_fn' f)
(ap_eq_of_fn_eq_fn' f)
(eq_of_fn_eq_fn'_ap f)
(inj' f)
(ap_inj' f)
(inj'_ap f)
end
@ -269,16 +269,16 @@ namespace is_equiv
include H
definition inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A}
(c : C (g' a)) : f⁻¹ (h' c) = h (f⁻¹ c) :=
eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
inj' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C (g' a)), f⁻¹ (h' c) = h (f⁻¹ c))
{a : A} (b : B (g' a)) : f (h b) = h' (f b) :=
eq_of_fn_eq_fn' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹)
inj' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹)
definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A}
(c : C (g' a)) : ap f (inv_commute' @f @h @h' p c)
= right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ :=
!ap_eq_of_fn_eq_fn'
!ap_inj'
-- inv_commute'_fn is in types.equiv
end
@ -286,7 +286,7 @@ namespace is_equiv
-- This is inv_commute' for A ≡ unit
definition inv_commute1' {B C : Type} (f : B → C) [is_equiv f] (h : B → B) (h' : C → C)
(p : Π(b : B), f (h b) = h' (f b)) (c : C) : f⁻¹ (h' c) = h (f⁻¹ c) :=
eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
inj' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
end is_equiv
open is_equiv
@ -350,12 +350,11 @@ namespace equiv
: A ≃ B :=
equiv.mk f (inv_homotopy_closed Heq)
--rename: eq_equiv_fn_eq_fn_of_is_equiv
definition eq_equiv_fn_eq [constructor] (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
definition eq_equiv_fn_eq_of_is_equiv [constructor] (f : A → B) [H : is_equiv f] (a b : A) :
(a = b) ≃ (f a = f b) :=
equiv.mk (ap f) !is_equiv_ap
--rename: eq_equiv_fn_eq_fn
definition eq_equiv_fn_eq_of_equiv [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
definition eq_equiv_fn_eq [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
equiv.mk (ap f) !is_equiv_ap
definition equiv_ap [constructor] (P : A → Type) {a b : A} (p : a = b) : P a ≃ P b :=
@ -368,17 +367,17 @@ namespace equiv
: equiv_of_eq (refl A) = equiv.refl A :=
idp
definition eq_of_fn_eq_fn [unfold 3] (f : A ≃ B) {x y : A} (q : f x = f y) : x = y :=
definition inj [unfold 3] (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 [unfold 3] (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y :=
definition inj_inv [unfold 3] (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y :=
(right_inv f x)⁻¹ ⬝ ap f q ⬝ right_inv f y
definition ap_eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
ap_eq_of_fn_eq_fn' f q
definition ap_inj (f : A ≃ B) {x y : A} (q : f x = f y) : ap f (inj' f q) = q :=
ap_inj' f q
definition eq_of_fn_eq_fn_ap (f : A ≃ B) {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q :=
eq_of_fn_eq_fn'_ap f q
definition inj_ap (f : A ≃ B) {x y : A} (q : x = y) : inj' f (ap f q) = q :=
inj'_ap f q
definition to_inv_homotopy_inv {f g : A ≃ B} (p : f ~ g) : f⁻¹ᵉ ~ g⁻¹ᵉ :=
inv_homotopy_inv p

2
hott/init/funext.hlean
View file

@ -239,7 +239,7 @@ end funext
open funext
namespace eq
definition eq_equiv_homotopy : (f = g) ≃ (f ~ g) :=
definition eq_equiv_homotopy (f g : Πx, P x) : (f = g) ≃ (f ~ g) :=
equiv.mk apd10 _
definition eq_of_homotopy [reducible] : f ~ g → f = g :=

2
hott/init/trunc.hlean
View file

@ -355,8 +355,6 @@ namespace is_trunc
theorem is_set.elimo (q q' : c =[p] c₂) [H : is_set (C a)] : q = q' :=
!is_prop.elim
-- TODO: port "Truncated morphisms"
/- truncated universe -/
end is_trunc

2
hott/init/ua.hlean
View file

@ -71,7 +71,7 @@ namespace equiv
rec_on_ua' f (λq, eq.rec_on q H)
definition ua_refl (A : Type) : ua erfl = idpath A :=
eq_of_fn_eq_fn !eq_equiv_equiv (right_inv !eq_equiv_equiv erfl)
inj !eq_equiv_equiv (right_inv !eq_equiv_equiv erfl)
definition ua_symm {A B : Type} (f : A ≃ B) : ua f⁻¹ᵉ = (ua f)⁻¹ :=
begin

16
hott/types/equiv.hlean
View file

@ -106,7 +106,7 @@ namespace is_equiv
inv_commute' @f @h @h' p (f b)
= (ap f⁻¹ (p b))⁻¹ ⬝ left_inv f (h b) ⬝ (ap h (left_inv f b))⁻¹ :=
begin
rewrite [↑[inv_commute',eq_of_fn_eq_fn'],+ap_con,-adj_inv f,+con.assoc,inv_con_cancel_left,
rewrite [↑[inv_commute',inj'],+ap_con,-adj_inv f,+con.assoc,inv_con_cancel_left,
adj f,+ap_inv,-+ap_compose,
eq_bot_of_square (natural_square_tr (λb, (left_inv f (h b))⁻¹ ⬝ ap f⁻¹ (p b)) (left_inv f b))⁻¹ʰ,
con_inv,inv_inv,+con.assoc],
@ -254,8 +254,8 @@ namespace equiv
definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') :=
calc
(f = f') ≃ (to_fun !equiv.sigma_char f = to_fun !equiv.sigma_char f')
: eq_equiv_fn_eq (to_fun !equiv.sigma_char)
(f = f') ≃ (!equiv.sigma_char f = !equiv.sigma_char f')
: eq_equiv_fn_eq !equiv.sigma_char
... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype
... ≃ (to_fun f = to_fun f') : equiv.rfl
@ -315,15 +315,15 @@ namespace equiv
[HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) :=
by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv
definition eq_of_fn_eq_fn'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A)
: eq_of_fn_eq_fn' f (idpath (f x)) = idpath x :=
definition inj'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A)
: inj' f (idpath (f x)) = idpath x :=
!con.left_inv
definition eq_of_fn_eq_fn'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A}
definition inj'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A}
(p : f x = f y) (q : f y = f z)
: eq_of_fn_eq_fn' f (p ⬝ q) = eq_of_fn_eq_fn' f p ⬝ eq_of_fn_eq_fn' f q :=
: inj' f (p ⬝ q) = inj' f p ⬝ inj' f q :=
begin
unfold eq_of_fn_eq_fn',
unfold inj',
refine _ ⬝ !con.assoc, apply whisker_right,
refine _ ⬝ !con.assoc⁻¹ ⬝ !con.assoc⁻¹, apply whisker_left,
refine !ap_con ⬝ _, apply whisker_left,

6
hott/types/fiber.hlean
View file

@ -31,7 +31,7 @@ namespace fiber
: (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
begin
apply equiv.trans,
apply eq_equiv_fn_eq_of_equiv, apply fiber.sigma_char,
apply eq_equiv_fn_eq, apply fiber.sigma_char,
apply equiv.trans,
apply sigma_eq_equiv,
apply sigma_equiv_sigma_right,
@ -180,7 +180,7 @@ namespace fiber
begin
fapply pequiv_of_equiv, esimp,
refine fiber.equiv_precompose f g (Point B),
esimp, apply (eq_of_fn_eq_fn (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
esimp, apply (inj (fiber.sigma_char _ _)), fapply sigma_eq: esimp,
{ apply respect_pt g },
{ apply eq_pathover_Fl' }
end
@ -210,7 +210,7 @@ namespace fiber
x = y ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) :=
calc
x = y ≃ fiber.sigma_char f b x = fiber.sigma_char f b y :
eq_equiv_fn_eq_of_equiv (fiber.sigma_char f b) x y
eq_equiv_fn_eq (fiber.sigma_char f b) x y
... ≃ Σ(p : point x = point y), point_eq x =[p] point_eq y : sigma_eq_equiv
... ≃ Σ(p : point x = point y), (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp :
sigma_equiv_sigma_right (λp,

6
hott/types/lift.hlean
View file

@ -142,10 +142,10 @@ namespace lift
fiber (lift_functor f) (up b) ≃ fiber f b :=
begin
fapply equiv.MK: intro v; cases v with a p,
{ cases a with a, exact fiber.mk a (eq_of_fn_eq_fn' up p) },
{ cases a with a, exact fiber.mk a (inj' up p) },
{ exact fiber.mk (up a) (ap up p) },
{ apply ap (fiber.mk a), apply eq_of_fn_eq_fn'_ap },
{ cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_eq_of_fn_eq_fn' }
{ apply ap (fiber.mk a), apply inj'_ap },
{ cases a with a, esimp, apply ap (fiber.mk (up a)), apply ap_inj' }
end
definition lift_functor2 {A B C : Type} (f : A → B → C) (x : lift A) (y : lift B) : lift C :=

12
hott/types/pi.hlean
View file

@ -58,7 +58,7 @@ namespace pi
/- Pathovers -/
definition pi_pathover {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
definition pi_pathover' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
(r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[apd011 C p q] g b') : f =[p] g :=
begin
cases p, apply pathover_idp_of_eq,
@ -66,7 +66,7 @@ namespace pi
apply eq_of_pathover_idp, apply r
end
definition pi_pathover_left {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
definition pi_pathover_left' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
(r : Π(b : B a), f b =[apd011 C p !pathover_tr] g (p ▸ b)) : f =[p] g :=
begin
cases p, apply pathover_idp_of_eq,
@ -74,7 +74,7 @@ namespace pi
apply eq_of_pathover_idp, apply r
end
definition pi_pathover_right {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
definition pi_pathover_right' {f : Πb, C a b} {g : Πb', C a' b'} {p : a = a'}
(r : Π(b' : B a'), f (p⁻¹ ▸ b') =[apd011 C p !tr_pathover] g b') : f =[p] g :=
begin
cases p, apply pathover_idp_of_eq,
@ -93,7 +93,7 @@ namespace pi
-- a version where C is uncurried, but where the conclusion of r is still a proper pathover
-- instead of a heterogenous equality
definition pi_pathover' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
definition pi_pathover {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
{p : a = a'} (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[dpair_eq_dpair p q] g b')
: f =[p] g :=
begin
@ -102,7 +102,7 @@ namespace pi
apply (@eq_of_pathover_idp _ C), exact (r b b (pathover.idpatho b)),
end
definition pi_pathover_left' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
definition pi_pathover_left {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
{p : a = a'} (r : Π(b : B a), f b =[dpair_eq_dpair p !pathover_tr] g (p ▸ b))
: f =[p] g :=
begin
@ -111,7 +111,7 @@ namespace pi
apply eq_of_pathover_idp, esimp at r, exact !pathover_ap (r b)
end
definition pi_pathover_right' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
definition pi_pathover_right {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb', C ⟨a', b'⟩}
{p : a = a'} (r : Π(b' : B a'), f (p⁻¹ ▸ b') =[dpair_eq_dpair p !tr_pathover] g b')
: f =[p] g :=
begin

54
hott/types/pointed.hlean
View file

@ -162,7 +162,7 @@ namespace pointed
{ induction x, reflexivity }
end
definition pmap.sigma_char [constructor] {A B : Type*} : (A →* B) ≃ Σ(f : A → B), f pt = pt :=
definition pmap.sigma_char [constructor] (A B : Type*) : (A →* B) ≃ Σ(f : A → B), f pt = pt :=
!ppi.sigma_char
definition pmap.eta_expand [constructor] {A B : Type*} (f : A →* B) : A →* B :=
@ -204,7 +204,7 @@ namespace pointed
definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B :=
pmap.mk (cast (ap pType.carrier p)) (by induction p; reflexivity)
definition pinverse [constructor] {X : Type*} : Ω X →* Ω X :=
definition pinverse [constructor] (X : Type*) : Ω X →* Ω X :=
pmap.mk eq.inverse idp
/-
@ -301,24 +301,16 @@ namespace pointed
intro p, exact !idp_con⁻¹
end
definition is_equiv_apn (n : ℕ) (f : A →* B) [H : is_equiv f]
: is_equiv (apn n f) :=
begin
induction n with n IH,
{ exact H},
{ exact is_equiv_ap1 (apn n f)}
end
definition pinverse_con [constructor] {X : Type*} (p q : Ω X)
: pinverse (p ⬝ q) = pinverse q ⬝ pinverse p :=
: pinverse X (p ⬝ q) = pinverse X q ⬝ pinverse X p :=
!con_inv
definition pinverse_inv [constructor] {X : Type*} (p : Ω X)
: pinverse p⁻¹ = (pinverse p)⁻¹ :=
: pinverse X p⁻¹ = (pinverse X p)⁻¹ :=
idp
definition ap1_pcompose_pinverse [constructor] {X Y : Type*} (f : X →* Y) :
Ω→ f ∘* pinverse ~* pinverse ∘* Ω→ f :=
Ω→ f ∘* pinverse X ~* pinverse Y ∘* Ω→ f :=
phomotopy.mk (ap1_gen_inv f (respect_pt f) (respect_pt f))
abstract begin
induction Y with Y y₀, induction f with f f₀, esimp at * ⊢, induction f₀, reflexivity
@ -437,7 +429,7 @@ namespace pointed
: sigma_equiv_sigma_right
(λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
... ≃ Σ(p : k ~ l), respect_pt k = p pt ⬝ respect_pt l
: sigma_equiv_sigma_left' eq_equiv_homotopy
: sigma_equiv_sigma_left' !eq_equiv_homotopy
... ≃ Σ(p : k ~ l), p pt ⬝ respect_pt l = respect_pt k
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ (k ~* l) : phomotopy.sigma_char k l
@ -640,7 +632,7 @@ namespace pointed
{ reflexivity}
end
definition ap1_pinverse [constructor] {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) :=
definition ap1_pinverse [constructor] {A : Type*} : ap1 (pinverse A) ~* pinverse (Ω A) :=
begin
fapply phomotopy.mk,
{ intro p, refine !idp_con ⬝ _, exact !inv_eq_inv2⁻¹ },
@ -715,7 +707,7 @@ namespace pointed
definition pcast_idp [constructor] {A : Type*} : pcast (idpath A) ~* pid A :=
by reflexivity
definition pinverse_pinverse (A : Type*) : pinverse ∘* pinverse ~* pid (Ω A) :=
definition pinverse_pinverse (A : Type*) : pinverse A ∘* pinverse A ~* pid (Ω A) :=
begin
fapply phomotopy.mk,
{ apply inv_inv},
@ -1051,7 +1043,6 @@ namespace pointed
/- pointed equivalences between particular pointed types -/
-- TODO: remove is_equiv_apn, which is proven again here
definition loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : Ω[n] A ≃* Ω[n] B :=
pequiv.MK (apn n f) (apn n f⁻¹ᵉ*)
abstract begin
@ -1073,9 +1064,15 @@ namespace pointed
apply ap1_pid}
end end
definition is_equiv_apn [constructor] (n : ℕ) (f : A →* B) (H : is_equiv f) : is_equiv (apn n f) :=
to_is_equiv (loopn_pequiv_loopn n (pequiv_of_pmap f H))
definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B :=
loopn_pequiv_loopn 1 f
notation `Ω≃`:(max+5) := loop_pequiv_loop
notation `Ω≃[`:95 n:0 `]`:0 := loopn_pequiv_loopn n
definition loop_pequiv_eq_closed [constructor] {A : Type} {a a' : A} (p : a = a')
: pointed.MK (a = a) idp ≃* pointed.MK (a' = a') idp :=
pequiv_of_equiv (loop_equiv_eq_closed p) (con.left_inv p)
@ -1121,7 +1118,7 @@ namespace pointed
end end
definition pequiv_pinverse (A : Type*) : Ω A ≃* Ω A :=
pequiv_of_pmap pinverse !is_equiv_eq_inverse
pequiv_of_pmap (pinverse A) !is_equiv_eq_inverse
definition pequiv_of_eq_pt [constructor] {A : Type} {a a' : A} (p : a = a') :
pointed.MK A a ≃* pointed.MK A a' :=
@ -1142,36 +1139,33 @@ namespace pointed
end
/- properties of iterated loop space -/
variable (A)
definition loopn_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) :=
definition loopn_succ_in (n : ℕ) (A : Type*) : Ω[succ n] A ≃* Ω[n] (Ω A) :=
begin
induction n with n IH,
{ reflexivity},
{ exact loop_pequiv_loop IH}
end
definition loopn_add (n m : ℕ) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) :=
definition loopn_add (n m : ℕ) (A : Type*) : Ω[n] (Ω[m] A) ≃* Ω[m+n] (A) :=
begin
induction n with n IH,
{ reflexivity},
{ exact loop_pequiv_loop IH}
end
definition loopn_succ_out (n : ℕ) : Ω[succ n] A ≃* Ω(Ω[n] A) :=
definition loopn_succ_out (n : ℕ) (A : Type*) : Ω[succ n] A ≃* Ω(Ω[n] A) :=
by reflexivity
variable {A}
definition loopn_succ_in_con {n : ℕ} (p q : Ω[succ (succ n)] A) :
loopn_succ_in A (succ n) (p ⬝ q) =
loopn_succ_in A (succ n) p ⬝ loopn_succ_in A (succ n) q :=
loopn_succ_in (succ n) A (p ⬝ q) =
loopn_succ_in (succ n) A p ⬝ loopn_succ_in (succ n) A q :=
!loop_pequiv_loop_con
definition loopn_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A :=
begin
intros, fapply pType_eq,
{ esimp, transitivity _,
apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹),
apply eq_equiv_fn_eq (equiv_eq_closed_right _ p⁻¹),
esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv},
{ esimp, apply con.left_inv}
end
@ -1185,7 +1179,7 @@ namespace pointed
... = Ω[n+2] A : by rewrite [algebra.add.comm]
definition apn_succ_phomotopy_in (n : ℕ) (f : A →* B) :
loopn_succ_in B n ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n :=
loopn_succ_in n B ∘* Ω→[n + 1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A :=
begin
induction n with n IH,
{ reflexivity},
@ -1193,11 +1187,11 @@ namespace pointed
end
definition loopn_succ_in_natural {A B : Type*} (n : ℕ) (f : A →* B) :
loopn_succ_in B n ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in A n :=
loopn_succ_in n B ∘* Ω→[n+1] f ~* Ω→[n] (Ω→ f) ∘* loopn_succ_in n A :=
!apn_succ_phomotopy_in
definition loopn_succ_in_inv_natural {A B : Type*} (n : ℕ) (f : A →* B) :
Ω→[n + 1] f ∘* (loopn_succ_in A n)⁻¹ᵉ* ~* (loopn_succ_in B n)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):=
Ω→[n + 1] f ∘* (loopn_succ_in n A)⁻¹ᵉ* ~* (loopn_succ_in n B)⁻¹ᵉ* ∘* Ω→[n] (Ω→ f):=
begin
apply pinv_right_phomotopy_of_phomotopy,
refine _ ⬝* !passoc⁻¹*,

18
hott/types/pointed2.hlean
View file

@ -48,10 +48,6 @@ namespace pointed
-- intro p,
-- end
/- Short term TODO: generalize to dependent maps (use ppi_eq_equiv?)
Long term TODO: use homotopies between pointed homotopies, not equalities
-/
definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) :
(h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h :=
@ -72,7 +68,7 @@ namespace pointed
: by exact sigma_equiv_sigma_right (λp, equiv_eq_closed_left _ (whisker_right _ (!whisker_right_ap⁻¹ᵖ)))
... ≃ Σ(p : to_homotopy h ~ to_homotopy k),
whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h
: sigma_equiv_sigma_left' eq_equiv_homotopy
: sigma_equiv_sigma_left' !eq_equiv_homotopy
definition phomotopy_eq {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k)
(q : whisker_right (respect_pt g) (p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h) : h = k :=
@ -448,7 +444,7 @@ namespace pointed
: f ~* g :=
begin
apply phomotopy.mk (λa, eq_of_phomotopy (p a)),
apply eq_of_fn_eq_fn (pmap_eq_equiv _ _), esimp [pmap_eq_equiv],
apply inj (pmap_eq_equiv _ _), esimp [pmap_eq_equiv],
refine !phomotopy_of_eq_con ⬝ _,
refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q,
end
@ -460,8 +456,8 @@ namespace pointed
definition ppcompose_right [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=
pmap.mk (λg, g ∘* f) (eq_of_phomotopy (pconst_pcompose f))
/- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof), rename to ppmap_pequiv_ppmap_right -/
definition pequiv_ppcompose_left [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
/- TODO: give construction using pequiv.MK, which computes better (see comment for a start of the proof) -/
definition ppmap_pequiv_ppmap_right [constructor] (g : B ≃* C) : ppmap A B ≃* ppmap A C :=
pequiv.MK' (ppcompose_left g) (ppcompose_left g⁻¹ᵉ*)
begin intro f, apply eq_of_phomotopy, apply pinv_pcompose_cancel_left end
begin intro f, apply eq_of_phomotopy, apply pcompose_pinv_cancel_left end
@ -477,7 +473,7 @@ namespace pointed
-- exact sorry
-- end end
definition pequiv_ppcompose_right [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C :=
definition ppmap_pequiv_ppmap_left [constructor] (f : A ≃* B) : ppmap B C ≃* ppmap A C :=
begin
fapply pequiv.MK',
{ exact ppcompose_right f },
@ -830,7 +826,7 @@ namespace pointed
fapply is_trunc_equiv_closed,
{ exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
fapply is_contr_fiber_of_is_equiv,
exact pequiv.to_is_equiv (pequiv_ppcompose_left f)
exact pequiv.to_is_equiv (ppmap_pequiv_ppmap_right f)
end
definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) :=
@ -838,7 +834,7 @@ namespace pointed
fapply is_trunc_equiv_closed,
{ exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) },
fapply is_contr_fiber_of_is_equiv,
exact pequiv.to_is_equiv (pequiv_ppcompose_right f)
exact pequiv.to_is_equiv (ppmap_pequiv_ppmap_left f)
end
definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g :=

5
hott/types/sigma.hlean
View file

@ -198,15 +198,14 @@ namespace sigma
: bc =[p] ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
by induction p; induction bc; apply idpo
-- TODO: interchange sigma_pathover and sigma_pathover'
definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b)
definition sigma_pathover' (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b)
(r : u.1 =[p] v.1) (s : u.2 =[apd011 C p r] v.2) : u =[p] v :=
begin
induction u, induction v, esimp at *, induction r,
esimp [apd011] at s, induction s using idp_rec_on, apply idpo
end
definition sigma_pathover' (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b)
definition sigma_pathover (p : a = a') (u : Σ(b : B a), C a b) (v : Σ(b : B a'), C a' b)
(r : u.1 =[p] v.1) (s : pathover (λx, C x.1 x.2) u.2 (sigma_eq p r) v.2) : u =[p] v :=
begin
induction u, induction v, esimp at *, induction r,

10
hott/types/trunc.hlean
View file

@ -325,7 +325,7 @@ namespace is_trunc
(A = B) ≃ (carrier A = carrier B) :=
calc
(A = B) ≃ (to_fun (trunctype.sigma_char n) A = to_fun (trunctype.sigma_char n) B)
: eq_equiv_fn_eq_of_equiv
: eq_equiv_fn_eq
... ≃ ((to_fun (trunctype.sigma_char n) A).1 = (to_fun (trunctype.sigma_char n) B).1)
: equiv.symm (!equiv_subtype)
... ≃ (carrier A = carrier B) : equiv.refl
@ -352,7 +352,7 @@ namespace is_trunc
definition tua_refl {n : ℕ₋₂} (A : n-Type) : tua (@erfl A) = idp :=
begin
refine ap (trunctype_eq_equiv n A A)⁻¹ᶠ (ua_refl A) ⬝ _,
refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_idp ,
refine ap (inj _) _ ⬝ !inj'_idp ,
apply ap (dpair_eq_dpair idp), apply is_prop.elim
end
@ -360,7 +360,7 @@ namespace is_trunc
: tua (f ⬝e g) = tua f ⬝ tua g :=
begin
refine ap (trunctype_eq_equiv n A C)⁻¹ᶠ (ua_trans f g) ⬝ _,
refine ap (eq_of_fn_eq_fn _) _ ⬝ !eq_of_fn_eq_fn'_con,
refine ap (inj _) _ ⬝ !inj'_con,
refine _ ⬝ !dpair_eq_dpair_con,
apply ap (dpair_eq_dpair _), esimp, apply is_prop.elim
end
@ -723,7 +723,7 @@ namespace trunc
end
definition is_equiv_trunc_functor_of_le {n k : ℕ₋₂} {A B : Type} (f : A → B) (H : n ≤ k)
[is_equiv (trunc_functor k f)] : is_equiv (trunc_functor n f) :=
(H' : is_equiv (trunc_functor k f)) : is_equiv (trunc_functor n f) :=
is_equiv_of_equiv_of_homotopy (trunc_equiv_trunc_of_le H (equiv.mk (trunc_functor k f) _))
(trunc_functor_homotopy_of_le f H)
@ -1116,7 +1116,7 @@ namespace function
apply is_equiv_of_imp_is_equiv,
intro p,
note q := ap (@tr 0 _) p,
note r := @(eq_of_fn_eq_fn' (trunc_functor 0 f)) _ (tr a) (tr a') q,
note r := @(inj' (trunc_functor 0 f)) _ (tr a) (tr a') q,
induction (tr_eq_tr_equiv _ _ _ r) with s,
induction s,
apply is_equiv.homotopy_closed (ap1 (pmap_of_map f a)),

2
hott/types/unit.hlean
View file

@ -42,7 +42,7 @@ namespace unit
definition unit_arrow_eq_compose {X Y : Type} (g : X → Y) (f : unit → X) :
unit_arrow_eq (g ∘ f) = ap (λf, g ∘ f) (unit_arrow_eq f) :=
begin
apply eq_of_fn_eq_fn' apd10,
apply inj' apd10,
refine right_inv apd10 _ ⬝ _,
refine _ ⬝ ap apd10 (!compose_eq_of_homotopy)⁻¹,
refine _ ⬝ (right_inv apd10 _)⁻¹,

2
tests/lean/extra/755.hlean
View file

@ -38,7 +38,7 @@ section
(Pe : Π(a a' : A), Pt a = Pt a') (a a' : A)
: 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')),
apply inj_inv !(pathover_constant (tr_eq a a')),
rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq],
end