132 lines
4.2 KiB
Text
132 lines
4.2 KiB
Text
-- definitions, theorems and attributes which should be moved to files in the HoTT library
|
||
|
||
import homotopy.sphere2 homotopy.cofiber homotopy.wedge
|
||
|
||
open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
|
||
is_trunc function sphere
|
||
|
||
namespace group
|
||
open is_trunc
|
||
|
||
-- some extra instances for type class inference
|
||
-- definition is_homomorphism_comm_homomorphism [instance] {G G' : AbGroup} (φ : G →g G')
|
||
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G))
|
||
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
|
||
-- homomorphism.struct φ
|
||
|
||
-- definition is_homomorphism_comm_homomorphism1 [instance] {G G' : AbGroup} (φ : G →g G')
|
||
-- : @is_homomorphism G G' _
|
||
-- (@ab_group.to_group _ (AbGroup.struct G')) φ :=
|
||
-- homomorphism.struct φ
|
||
|
||
-- definition is_homomorphism_comm_homomorphism2 [instance] {G G' : AbGroup} (φ : G →g G')
|
||
-- : @is_homomorphism G G' (@ab_group.to_group _ (AbGroup.struct G)) _ φ :=
|
||
-- homomorphism.struct φ
|
||
|
||
end group open group
|
||
|
||
|
||
namespace pi -- move to types.arrow
|
||
|
||
definition pmap_eq_idp {X Y : Type*} (f : X →* Y) :
|
||
pmap_eq (λx, idpath (f x)) !idp_con⁻¹ = idpath f :=
|
||
begin
|
||
cases f with f p, esimp [pmap_eq],
|
||
refine apd011 (apd011 pmap.mk) !eq_of_homotopy_idp _,
|
||
induction Y with Y y0, esimp at *, induction p, esimp, exact sorry
|
||
end
|
||
|
||
definition pfunext [constructor] (X Y : Type*) : ppmap X (Ω Y) ≃* Ω (ppmap X Y) :=
|
||
begin
|
||
fapply pequiv_of_equiv,
|
||
{ fapply equiv.MK: esimp,
|
||
{ intro f, fapply pmap_eq,
|
||
{ intro x, exact f x },
|
||
{ exact (respect_pt f)⁻¹ }},
|
||
{ intro p, fapply pmap.mk,
|
||
{ intro x, exact ap010 pmap.to_fun p x },
|
||
{ note z := apd respect_pt p,
|
||
note z2 := square_of_pathover z,
|
||
refine eq_of_hdeg_square z2 ⬝ !ap_constant }},
|
||
{ intro p, exact sorry },
|
||
{ intro p, exact sorry }},
|
||
{ apply pmap_eq_idp}
|
||
end
|
||
|
||
end pi open pi
|
||
|
||
namespace eq
|
||
|
||
-- definition natural_square_tr_eq {A B : Type} {a a' : A} {f g : A → B}
|
||
-- (p : f ~ g) (q : a = a') : natural_square p q = square_of_pathover (apd p q) :=
|
||
-- idp
|
||
|
||
end eq open eq
|
||
|
||
namespace pointed
|
||
|
||
-- /- the pointed type of (unpointed) dependent maps -/
|
||
-- definition pupi [constructor] {A : Type} (P : A → Type*) : Type* :=
|
||
-- pointed.mk' (Πa, P a)
|
||
|
||
-- definition loop_pupi_commute {A : Type} (B : A → Type*) : Ω(pupi B) ≃* pupi (λa, Ω (B a)) :=
|
||
-- pequiv_of_equiv eq_equiv_homotopy rfl
|
||
|
||
-- definition equiv_pupi_right {A : Type} {P Q : A → Type*} (g : Πa, P a ≃* Q a)
|
||
-- : pupi P ≃* pupi Q :=
|
||
-- pequiv_of_equiv (pi_equiv_pi_right g)
|
||
-- begin esimp, apply eq_of_homotopy, intros a, esimp, exact (respect_pt (g a)) end
|
||
|
||
end pointed open pointed
|
||
|
||
namespace fiber
|
||
|
||
|
||
definition ap1_ppoint_phomotopy {A B : Type*} (f : A →* B)
|
||
: Ω→ (ppoint f) ∘* pfiber_loop_space f ~* ppoint (Ω→ f) :=
|
||
begin
|
||
exact sorry
|
||
end
|
||
|
||
definition pfiber_equiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D}
|
||
(h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h)
|
||
: ppoint g ∘* pfiber_equiv_of_square h k s ~* h ∘* ppoint f :=
|
||
sorry
|
||
|
||
end fiber
|
||
|
||
namespace circle
|
||
|
||
|
||
/-
|
||
Suppose for `f, g : A -> B` I prove a homotopy `H : f ~ g` by induction on the element in `A`.
|
||
And suppose `p : a = a'` is a path constructor in `A`.
|
||
Then `natural_square_tr H p` has type `square (H a) (H a') (ap f p) (ap g p)` and is equal
|
||
to the square which defined H on the path constructor
|
||
-/
|
||
|
||
definition natural_square_elim_loop {A : Type} {f g : S¹ → A} (p : f base = g base)
|
||
(q : square p p (ap f loop) (ap g loop))
|
||
: natural_square (circle.rec p (eq_pathover q)) loop = q :=
|
||
begin
|
||
-- refine !natural_square_eq ⬝ _,
|
||
refine ap square_of_pathover !rec_loop ⬝ _,
|
||
exact to_right_inv !eq_pathover_equiv_square q
|
||
end
|
||
|
||
|
||
end circle
|
||
|
||
namespace sphere
|
||
|
||
-- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
|
||
-- f ~* pconst (S* n) (S* m) :=
|
||
-- begin
|
||
-- assert H : is_contr (Ω[n] (S* m)),
|
||
-- { apply homotopy_group_sphere_le, },
|
||
-- apply phomotopy_of_eq,
|
||
-- apply eq_of_fn_eq_fn !psphere_pmap_pequiv,
|
||
-- apply @is_prop.elim
|
||
-- end
|
||
|
||
end sphere
|