diff --git a/hott/algebra/bundled.hlean b/hott/algebra/bundled.hlean index cb6942964..a03ddaeb3 100644 --- a/hott/algebra/bundled.hlean +++ b/hott/algebra/bundled.hlean @@ -5,7 +5,7 @@ Authors: Jeremy Avigad Bundled structures -/ -import algebra.group +import algebra.ring open algebra pointed is_trunc namespace algebra @@ -34,64 +34,82 @@ attribute CommMonoid.carrier [coercion] attribute CommMonoid.struct [instance] structure Group := -(carrier : Type) (struct : group carrier) +(carrier : Type) (struct' : group carrier) -attribute Group.carrier [coercion] -attribute Group.struct [instance] +attribute Group.struct' [instance] section - local attribute Group.struct [instance] - definition pSet_of_Group [constructor] [reducible] [coercion] (G : Group) : Set* := - ptrunctype.mk G !semigroup.is_set_carrier 1 +local attribute Group.carrier [coercion] +definition pSet_of_Group [constructor] [reducible] [coercion] (G : Group) : Set* := +ptrunctype.mk (Group.carrier G) !semigroup.is_set_carrier 1 end +definition Group.struct [instance] [priority 2000] (G : Group) : group G := +Group.struct' G + attribute algebra._trans_of_pSet_of_Group [unfold 1] attribute algebra._trans_of_pSet_of_Group_1 algebra._trans_of_pSet_of_Group_2 [constructor] -definition pType_of_Group [reducible] [constructor] : Group → Type* := -algebra._trans_of_pSet_of_Group_1 -definition Set_of_Group [reducible] [constructor] : Group → Set := -algebra._trans_of_pSet_of_Group_2 +definition pType_of_Group [reducible] [constructor] (G : Group) : Type* := +G +definition Set_of_Group [reducible] [constructor] (G : Group) : Set := +G definition AddGroup : Type := Group +definition pSet_of_AddGroup [constructor] [reducible] [coercion] (G : AddGroup) : Set* := +pSet_of_Group G + definition AddGroup.mk [constructor] [reducible] (G : Type) (H : add_group G) : AddGroup := Group.mk G H -definition AddGroup.struct [reducible] (G : AddGroup) : add_group G := +definition AddGroup.struct [reducible] [instance] [priority 2000] (G : AddGroup) : add_group G := Group.struct G -attribute AddGroup.struct Group.struct [instance] [priority 2000] +attribute algebra._trans_of_pSet_of_AddGroup [unfold 1] +attribute algebra._trans_of_pSet_of_AddGroup_1 algebra._trans_of_pSet_of_AddGroup_2 [constructor] + +definition pType_of_AddGroup [reducible] [constructor] : AddGroup → Type* := +algebra._trans_of_pSet_of_AddGroup_1 +definition Set_of_AddGroup [reducible] [constructor] : AddGroup → Set := +algebra._trans_of_pSet_of_AddGroup_2 structure AbGroup := -(carrier : Type) (struct : ab_group carrier) +(carrier : Type) (struct' : ab_group carrier) -attribute AbGroup.carrier [coercion] - -definition AddAbGroup : Type := AbGroup - -definition AddAbGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_group G) : - AddAbGroup := -AbGroup.mk G H - -definition AddAbGroup.struct [reducible] (G : AddAbGroup) : add_ab_group G := -AbGroup.struct G - -attribute AddAbGroup.struct AbGroup.struct [instance] [priority 2000] +attribute AbGroup.struct' [instance] +section +local attribute AbGroup.carrier [coercion] definition Group_of_AbGroup [coercion] [constructor] (G : AbGroup) : Group := Group.mk G _ +end + +definition AbGroup.struct [instance] [priority 2000] (G : AbGroup) : ab_group G := +AbGroup.struct' G attribute algebra._trans_of_Group_of_AbGroup_1 algebra._trans_of_Group_of_AbGroup algebra._trans_of_Group_of_AbGroup_3 [constructor] attribute algebra._trans_of_Group_of_AbGroup_2 [unfold 1] -definition ab_group_AbGroup [instance] (G : AbGroup) : ab_group G := +definition AddAbGroup : Type := AbGroup + +definition AddGroup_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : AddGroup := +Group_of_AbGroup G + +definition AddAbGroup.struct [reducible] [instance] [priority 2000] (G : AddAbGroup) : + add_ab_group G := AbGroup.struct G -definition add_ab_group_AddAbGroup [instance] (G : AddAbGroup) : add_ab_group G := -AbGroup.struct G +definition AddAbGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_group G) : + AddAbGroup := +AbGroup.mk G H + +attribute algebra._trans_of_AddGroup_of_AddAbGroup_1 + algebra._trans_of_AddGroup_of_AddAbGroup + algebra._trans_of_AddGroup_of_AddAbGroup_3 [constructor] +attribute algebra._trans_of_AddGroup_of_AddAbGroup_2 [unfold 1] -- structure AddSemigroup := -- (carrier : Type) (struct : add_semigroup carrier) @@ -132,21 +150,26 @@ AbGroup.struct G -- some bundled infinity-structures structure InfGroup := -(carrier : Type) (struct : inf_group carrier) +(carrier : Type) (struct' : inf_group carrier) -attribute InfGroup.carrier [coercion] -attribute InfGroup.struct [instance] +attribute InfGroup.struct' [instance] section - local attribute InfGroup.struct [instance] + local attribute InfGroup.carrier [coercion] definition pType_of_InfGroup [constructor] [reducible] [coercion] (G : InfGroup) : Type* := pType.mk G 1 end attribute algebra._trans_of_pType_of_InfGroup [unfold 1] +definition InfGroup.struct [instance] [priority 2000] (G : InfGroup) : inf_group G := +InfGroup.struct' G + definition AddInfGroup : Type := InfGroup +definition pType_of_AddInfGroup [constructor] [reducible] [coercion] (G : AddInfGroup) : Type* := +pType_of_InfGroup G + definition AddInfGroup.mk [constructor] [reducible] (G : Type) (H : add_inf_group G) : AddInfGroup := InfGroup.mk G H @@ -154,29 +177,40 @@ InfGroup.mk G H definition AddInfGroup.struct [reducible] (G : AddInfGroup) : add_inf_group G := InfGroup.struct G -attribute AddInfGroup.struct InfGroup.struct [instance] [priority 2000] +attribute algebra._trans_of_pType_of_AddInfGroup [unfold 1] structure AbInfGroup := -(carrier : Type) (struct : ab_inf_group carrier) +(carrier : Type) (struct' : ab_inf_group carrier) -attribute AbInfGroup.carrier [coercion] +attribute AbInfGroup.struct' [instance] + +section +local attribute AbInfGroup.carrier [coercion] +definition InfGroup_of_AbInfGroup [coercion] [constructor] (G : AbInfGroup) : InfGroup := +InfGroup.mk G _ +end + +definition AbInfGroup.struct [instance] [priority 2000] (G : AbInfGroup) : ab_inf_group G := +AbInfGroup.struct' G + +attribute algebra._trans_of_InfGroup_of_AbInfGroup_1 [constructor] +attribute algebra._trans_of_InfGroup_of_AbInfGroup [unfold 1] definition AddAbInfGroup : Type := AbInfGroup +definition AddInfGroup_of_AddAbInfGroup [coercion] [constructor] (G : AddAbInfGroup) : AddInfGroup := +InfGroup_of_AbInfGroup G + +definition AddAbInfGroup.struct [reducible] [instance] [priority 2000] (G : AddAbInfGroup) : + add_ab_inf_group G := +AbInfGroup.struct G + definition AddAbInfGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_inf_group G) : AddAbInfGroup := AbInfGroup.mk G H -definition AddAbInfGroup.struct [reducible] (G : AddAbInfGroup) : add_ab_inf_group G := -AbInfGroup.struct G - -attribute AddAbInfGroup.struct AbInfGroup.struct [instance] [priority 2000] - -definition InfGroup_of_AbInfGroup [coercion] [constructor] (G : AbInfGroup) : InfGroup := -InfGroup.mk G _ - -attribute algebra._trans_of_InfGroup_of_AbInfGroup_1 [constructor] -attribute algebra._trans_of_InfGroup_of_AbInfGroup [unfold 1] +attribute algebra._trans_of_AddInfGroup_of_AddAbInfGroup_1 [constructor] +attribute algebra._trans_of_AddInfGroup_of_AddAbInfGroup [unfold 1] definition InfGroup_of_Group [constructor] (G : Group) : InfGroup := InfGroup.mk G _ @@ -190,4 +224,11 @@ AbInfGroup.mk G _ definition AddAbInfGroup_of_AddAbGroup [constructor] (G : AddAbGroup) : AddAbInfGroup := AddAbInfGroup.mk G _ +/- rings -/ +structure Ring := +(carrier : Type) (struct : ring carrier) + +attribute Ring.carrier [coercion] +attribute Ring.struct [instance] + end algebra diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean index fc51ac1bc..704496bd5 100644 --- a/hott/algebra/category/constructions/set.hlean +++ b/hott/algebra/category/constructions/set.hlean @@ -48,10 +48,10 @@ namespace category local attribute is_equiv_iso_of_equiv [instance] - definition iso_of_eq_eq_compose (A B : Set) : @iso_of_eq _ _ A B = + definition iso_of_eq_eq_compose (A B : Set) : @iso_of_eq _ _ A B ~ @iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘ @ap _ _ (to_fun (trunctype.sigma_char 0)) A B := - eq_of_homotopy (λp, eq.rec_on p idp) + λp, eq.rec_on p idp definition equiv_equiv_iso (A B : set) : (A ≃ B) ≃ (A ≅ B) := equiv.MK (λf, iso_of_equiv f) @@ -75,11 +75,8 @@ namespace category (@is_equiv_subtype_eq_inv _ _ _ _ _)) !univalence) !is_equiv_iso_of_equiv, - let H₂ := (iso_of_eq_eq_compose A B)⁻¹ in - begin - rewrite H₂ at H₁, - assumption - end + is_equiv.homotopy_closed _ (iso_of_eq_eq_compose A B)⁻¹ʰᵗʸ + end set definition category_Set [instance] [constructor] : category Set := diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index f32eb8a7a..e3b1aa2ce 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -18,10 +18,6 @@ namespace group definition Group.struct' [instance] [reducible] (G : Group) : group G := Group.struct G - definition ab_group_Group_of_AbGroup [instance] [constructor] [priority 900] - (G : AbGroup) : ab_group (Group_of_AbGroup G) := - begin esimp, exact _ end - definition ab_group_pSet_of_Group [instance] (G : AbGroup) : ab_group (pSet_of_Group G) := AbGroup.struct G @@ -29,74 +25,21 @@ namespace group group (pSet_of_Group G) := Group.struct G - /- group homomorphisms -/ -/- - definition is_homomorphism [class] [reducible] - {G₁ G₂ : Type} [has_mul G₁] [has_mul G₂] (φ : G₁ → G₂) : Type := - Π(g h : G₁), φ (g * h) = φ g * φ h + /- left and right actions -/ + definition is_equiv_mul_right [constructor] {A : Group} (a : A) : is_equiv (λb, b * a) := + adjointify _ (λb : A, b * a⁻¹) (λb, !inv_mul_cancel_right) (λb, !mul_inv_cancel_right) - section - variables {G G₁ G₂ G₃ : Type} {g h : G₁} (ψ : G₂ → G₃) {φ₁ φ₂ : G₁ → G₂} (φ : G₁ → G₂) - [group G] [group G₁] [group G₂] [group G₃] - [is_homomorphism ψ] [is_homomorphism φ₁] [is_homomorphism φ₂] [is_homomorphism φ] + definition right_action [constructor] {A : Group} (a : A) : A ≃ A := + equiv.mk _ (is_equiv_mul_right a) - definition respect_mul {G₁ G₂ : Type} [has_mul G₁] [has_mul G₂] (φ : G₁ → G₂) - [is_homomorphism φ] : Π(g h : G₁), φ (g * h) = φ g * φ h := - by assumption + definition is_equiv_add_right [constructor] {A : AddGroup} (a : A) : is_equiv (λb, b + a) := + adjointify _ (λb : A, b - a) (λb, !neg_add_cancel_right) (λb, !add_neg_cancel_right) - theorem respect_one /- φ -/ : φ 1 = 1 := - mul.right_cancel - (calc - φ 1 * φ 1 = φ (1 * 1) : respect_mul φ - ... = φ 1 : ap φ !one_mul - ... = 1 * φ 1 : one_mul) + definition add_right_action [constructor] {A : AddGroup} (a : A) : A ≃ A := + equiv.mk _ (is_equiv_add_right a) - theorem respect_inv /- φ -/ (g : G₁) : φ g⁻¹ = (φ g)⁻¹ := - eq_inv_of_mul_eq_one (!respect_mul⁻¹ ⬝ ap φ !mul.left_inv ⬝ !respect_one) + /- homomorphisms -/ - definition is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ := - begin - apply function.is_embedding_of_is_injective, - intro g g' p, - apply eq_of_mul_inv_eq_one, - apply H, - refine !respect_mul ⬝ _, - rewrite [respect_inv φ, p], - apply mul.right_inv - end - - definition is_homomorphism_compose {ψ : G₂ → G₃} {φ : G₁ → G₂} - (H1 : is_homomorphism ψ) (H2 : is_homomorphism φ) : is_homomorphism (ψ ∘ φ) := - λg h, ap ψ !respect_mul ⬝ !respect_mul - - definition is_homomorphism_id (G : Type) [group G] : is_homomorphism (@id G) := - λg h, idp - - end - - section additive - - definition is_add_homomorphism [class] [reducible] {G₁ G₂ : Type} [has_add G₁] [has_add G₂] - (φ : G₁ → G₂) : Type := - Π(g h : G₁), φ (g + h) = φ g + φ h - - variables {G₁ G₂ : Type} (φ : G₁ → G₂) [add_group G₁] [add_group G₂] [is_add_homomorphism φ] - - definition respect_add /- φ -/ : Π(g h : G₁), φ (g + h) = φ g + φ h := - by assumption - - theorem respect_zero /- φ -/ : φ 0 = 0 := - add.right_cancel - (calc - φ 0 + φ 0 = φ (0 + 0) : respect_add φ - ... = φ 0 : ap φ !zero_add - ... = 0 + φ 0 : zero_add) - - theorem respect_neg /- φ -/ (g : G₁) : φ (-g) = -(φ g) := - eq_neg_of_add_eq_zero (!respect_add⁻¹ ⬝ ap φ !add.left_inv ⬝ !respect_zero) - - end additive --/ structure homomorphism (G₁ G₂ : Group) : Type := (φ : G₁ → G₂) (p : is_mul_hom φ) @@ -277,33 +220,102 @@ namespace group infixl ` ⬝gp `:75 := isomorphism.trans_eq infixl ` ⬝pg `:75 := isomorphism.eq_trans - definition pmap_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : - G₁ →* G₂ := + definition pmap_of_isomorphism [constructor] (φ : G₁ ≃g G₂) : G₁ →* G₂ := pequiv_of_isomorphism φ - /- category of groups -/ + definition to_fun_isomorphism_trans {G H K : Group} (φ : G ≃g H) (ψ : H ≃g K) : + φ ⬝g ψ ~ ψ ∘ φ := + by reflexivity - section - open category - definition precategory_group [constructor] : precategory Group := - precategory.mk homomorphism - @homomorphism_compose - @homomorphism_id - (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp)) - (λG₁ G₂ φ, homomorphism_eq (λg, idp)) - (λG₁ G₂ φ, homomorphism_eq (λg, idp)) + definition add_homomorphism (G H : AddGroup) : Type := homomorphism G H + infix ` →a `:55 := add_homomorphism + + definition agroup_fun [coercion] [unfold 3] [reducible] {G H : AddGroup} (φ : G →a H) : G → H := + φ + + definition add_homomorphism.struct [instance] {G H : AddGroup} (φ : G →a H) : is_add_hom φ := + homomorphism.addstruct φ + + definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →g H := + homomorphism.mk φ h + + definition add_homomorphism_compose [constructor] [trans] {G₁ G₂ G₃ : AddGroup} + (ψ : G₂ →a G₃) (φ : G₁ →a G₂) : G₁ →a G₃ := + add_homomorphism.mk (ψ ∘ φ) (is_add_hom_compose _ _) + + definition add_homomorphism_id [constructor] [refl] (G : AddGroup) : G →a G := + add_homomorphism.mk (@id G) (is_add_hom_id G) + + abbreviation aid [constructor] := @add_homomorphism_id + infixr ` ∘a `:75 := add_homomorphism_compose + + definition to_respect_add' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g h : H₁) : χ (g + h) = χ g + χ h := + respect_add χ g h + + theorem to_respect_zero' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) : χ 0 = 0 := + respect_zero χ + + theorem to_respect_neg' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g : H₁) : χ (-g) = -(χ g) := + respect_neg χ g + + definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →a H) : G →a H := + add_homomorphism.mk (λg, φ g + ψ g) + abstract begin + intro g g', refine ap011 add !to_respect_add' !to_respect_add' ⬝ _, + refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x + _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹ + end end + + definition homomorphism_mul [constructor] {G H : AbGroup} (φ ψ : G →g H) : G →g H := + homomorphism.mk (λg, φ g * ψ g) (to_respect_add (homomorphism_add φ ψ)) + + definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G := + begin + fapply phomotopy_of_homotopy, reflexivity end - -- TODO - -- definition category_group : category Group := - -- category.mk precategory_group - -- begin - -- intro G₁ G₂, - -- fapply adjointify, - -- { intro φ, fapply Group_eq, }, - -- { }, - -- { } - -- end + definition pmap_of_homomorphism_gcompose {G H K : Group} (ψ : H →g K) (φ : G →g H) + : pmap_of_homomorphism (ψ ∘g φ) ~* pmap_of_homomorphism ψ ∘* pmap_of_homomorphism φ := + begin + fapply phomotopy_of_homotopy, reflexivity + end + + definition pmap_of_homomorphism_phomotopy {G H : Group} {φ ψ : G →g H} (H : φ ~ ψ) + : pmap_of_homomorphism φ ~* pmap_of_homomorphism ψ := + begin + fapply phomotopy_of_homotopy, exact H + end + + definition pequiv_of_isomorphism_trans {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ ≃g G₂) : + pequiv_of_isomorphism (φ ⬝g ψ) ~* pequiv_of_isomorphism ψ ∘* pequiv_of_isomorphism φ := + begin + apply phomotopy_of_homotopy, reflexivity + end + + definition isomorphism_eq {G H : Group} {φ ψ : G ≃g H} (p : φ ~ ψ) : φ = ψ := + begin + induction φ with φ φe, induction ψ with ψ ψe, + exact apd011 isomorphism.mk (homomorphism_eq p) !is_prop.elimo + end + + definition is_set_isomorphism [instance] (G H : Group) : is_set (G ≃g H) := + begin + have H : G ≃g H ≃ Σ(f : G →g H), is_equiv f, + begin + fapply equiv.MK, + { intro φ, induction φ, constructor, assumption }, + { intro v, induction v, constructor, assumption }, + { intro v, induction v, reflexivity }, + { intro φ, induction φ, reflexivity } + end, + apply is_trunc_equiv_closed_rev, exact H + end + + definition trivial_homomorphism (A B : Group) : A →g B := + homomorphism.mk (λa, 1) (λa a', (mul_one 1)⁻¹) + + definition trivial_add_homomorphism (A B : AddGroup) : A →a B := + homomorphism.mk (λa, 0) (λa a', (add_zero 0)⁻¹) + /- given an equivalence A ≃ B we can transport a group structure on A to a group structure on B -/ @@ -347,19 +359,43 @@ namespace group end + section + variables {A B : Type} (f : A ≃ B) [ab_group A] + definition group_equiv_mul_comm (b b' : B) : group_equiv_mul f b b' = group_equiv_mul f b' b := + by rewrite [↑group_equiv_mul, mul.comm] + + definition ab_group_equiv_closed : ab_group B := + ⦃ab_group, group_equiv_closed f, + mul_comm := group_equiv_mul_comm f⦄ + end + variable (G) /- the trivial group -/ open unit - --rename: group_unit - definition trivial_group [constructor] : group unit := + definition group_unit [constructor] : group unit := group.mk _ (λx y, star) (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) - --rename trivial_group - definition Trivial_group [constructor] : Group := - Group.mk _ trivial_group + definition ab_group_unit [constructor] : ab_group unit := + ⦃ab_group, group_unit, mul_comm := λx y, idp⦄ - abbreviation G0 := Trivial_group + definition trivial_group [constructor] : Group := + Group.mk _ group_unit + + abbreviation G0 := trivial_group + + definition AbGroup_of_Group.{u} (G : Group.{u}) (H : Π x y : G, x * y = y * x) : AbGroup.{u} := + begin + induction G, + fapply AbGroup.mk, + assumption, + exact ⦃ab_group, struct', mul_comm := H⦄ + end + + definition trivial_ab_group : AbGroup.{0} := + begin + fapply AbGroup_of_Group trivial_group, intro x y, reflexivity + end definition trivial_group_of_is_contr [H : is_contr G] : G ≃g G0 := begin @@ -368,6 +404,33 @@ namespace group { intros, reflexivity} end + definition ab_group_of_is_contr (A : Type) [is_contr A] : ab_group A := + have ab_group unit, from ab_group_unit, + ab_group_equiv_closed (equiv_unit_of_is_contr A)⁻¹ᵉ + + definition group_of_is_contr (A : Type) [is_contr A] : group A := + have ab_group A, from ab_group_of_is_contr A, by apply _ + + definition ab_group_lift_unit : ab_group (lift unit) := + ab_group_of_is_contr (lift unit) + + definition trivial_ab_group_lift : AbGroup := + AbGroup.mk _ ab_group_lift_unit + + definition from_trivial_ab_group (A : AbGroup) : trivial_ab_group →g A := + trivial_homomorphism trivial_ab_group A + + definition is_embedding_from_trivial_ab_group (A : AbGroup) : + is_embedding (from_trivial_ab_group A) := + begin + fapply is_embedding_of_is_injective, + intro x y p, + induction x, induction y, reflexivity + end + + definition to_trivial_ab_group (A : AbGroup) : A →g trivial_ab_group := + trivial_homomorphism A trivial_ab_group + variable {G} /- diff --git a/hott/algebra/homomorphism.hlean b/hott/algebra/homomorphism.hlean index e65b7d2e1..971e5efad 100644 --- a/hott/algebra/homomorphism.hlean +++ b/hott/algebra/homomorphism.hlean @@ -58,11 +58,17 @@ section add_group_A_B have x₁ - x₂ = 0, from H _ this, eq_of_sub_eq_zero this) - definition eq_zero_of_is_add_hom [add_group B] {f : A → B} [is_add_hom f] + definition eq_zero_of_is_add_hom {f : A → B} [is_add_hom f] [is_embedding f] {a : A} (fa0 : f a = 0) : a = 0 := have f a = f 0, by rewrite [fa0, respect_zero f], show a = 0, from is_injective_of_is_embedding this + + theorem eq_zero_of_eq_zero_of_is_embedding {f : A → B} [is_add_hom f] [is_embedding f] + {a : A} (h : f a = 0) : a = 0 := + have f a = f 0, by rewrite [h, respect_zero], + show a = 0, from is_injective_of_is_embedding this + end add_group_A_B /- multiplicative structures -/ diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index ccae57859..781294c72 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -23,6 +23,12 @@ namespace eq definition ab_inf_group_loop [constructor] [instance] (A : Type*) : ab_inf_group (Ω (Ω A)) := ⦃ab_inf_group, inf_group_loop _, mul_comm := eckmann_hilton⦄ + definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) := + by induction H; exact _ + + definition ab_inf_group_loopn (n : ℕ) (A : Type*) [H : is_at_least_two n] : ab_inf_group (Ω[n] A) := + by induction H; exact _ + definition gloop [constructor] (A : Type*) : InfGroup := InfGroup.mk (Ω A) (inf_group_loop A) @@ -124,6 +130,13 @@ namespace eq { 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) := + begin + apply is_trunc_trunc_of_is_trunc, + apply is_contr_loop_of_is_trunc, + apply is_trunc_of_is_contr + end + definition homotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B) : π[n] A →* π[n] B := ptrunc_functor 0 (apn n f) @@ -195,6 +208,12 @@ namespace eq notation `π→g[`:95 n:0 `]`:0 := homotopy_group_homomorphism n + 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) + 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 diff --git a/hott/algebra/inf_group.hlean b/hott/algebra/inf_group.hlean index e2ccb70a0..5a8009b43 100644 --- a/hott/algebra/inf_group.hlean +++ b/hott/algebra/inf_group.hlean @@ -331,6 +331,9 @@ section inf_group ⦃ right_cancel_inf_semigroup, s, mul_right_cancel := @mul_right_cancel A s ⦄ + definition one_unique {a : A} (H : Πb, a * b = b) : a = 1 := + !mul_one⁻¹ ⬝ H 1 + end inf_group structure ab_inf_group [class] (A : Type) extends inf_group A, comm_inf_monoid A @@ -533,6 +536,9 @@ section add_inf_group theorem add_eq_of_eq_sub {a b c : A} (H : a = c - b) : a + b = c := add_eq_of_eq_add_neg H + definition zero_unique {a : A} (H : Πb, a + b = b) : a = 0 := + !add_zero⁻¹ ⬝ H 0 + end add_inf_group definition add_ab_inf_group [class] : Type → Type := ab_inf_group diff --git a/hott/arity.hlean b/hott/arity.hlean index 88ed2b08e..946b8e88a 100644 --- a/hott/arity.hlean +++ b/hott/arity.hlean @@ -137,6 +137,18 @@ namespace eq ap010 f (ap g p) a = ap010 (λy, f (g y)) p a := eq.rec_on p idp + definition ap_eq_ap010 {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : + ap (λa, f a b) p = ap010 f p b := + by reflexivity + + definition ap011_idp {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') (b : B) : + ap011 f p idp = ap010 f p b := + by reflexivity + + definition ap011_flip {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B} (p : a = a') (q : b = b') : + ap011 f p q = ap011 (λb a, f a b) q p := + by induction q; induction p; reflexivity + /- the following theorems are function extentionality for functions with multiple arguments -/ definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ~2 g) : f = g := diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean index c213e1778..6d476e058 100644 --- a/hott/cubical/cube.hlean +++ b/hott/cubical/cube.hlean @@ -347,4 +347,42 @@ namespace eq infixr ` ⬝p3 `:75 := eq_concat3 infixl ` ⬝3p `:75 := concat3_eq + definition whisker001 {p₀₀₁' : a₀₀₀ = a₀₀₂} (q : p₀₀₁' = p₀₀₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube (q ⬝ph s₀₁₁) s₂₁₁ (q ⬝ph s₁₀₁) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker021 {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁' = p₀₂₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube (s₀₁₁ ⬝hp q⁻¹) s₂₁₁ s₁₀₁ (q ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker021' {p₀₂₁' : a₀₂₀ = a₀₂₂} (q : p₀₂₁ = p₀₂₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube (s₀₁₁ ⬝hp q) s₂₁₁ s₁₀₁ (q⁻¹ ⬝ph s₁₂₁) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker201 {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁' = p₂₀₁) + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ (q ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q⁻¹) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker201' {p₂₀₁' : a₂₀₀ = a₂₀₂} (q : p₂₀₁ = p₂₀₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ (q⁻¹ ⬝ph s₂₁₁) (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition whisker221 {p₂₂₁' : a₂₂₀ = a₂₂₂} (q : p₂₂₁ = p₂₂₁') + (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ (s₁₂₁ ⬝hp q) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition move221 {p₂₂₁' : a₂₂₀ = a₂₂₂} {s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁'} (q : p₂₂₁ = p₂₂₁') + (c : cube s₀₁₁ (s₂₁₁ ⬝hp q) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ s₂₁₁ s₁₀₁ (s₁₂₁ ⬝hp q⁻¹) s₁₁₀ s₁₁₂ := + by induction q; exact c + + definition move201 {p₂₀₁' : a₂₀₀ = a₂₀₂} {s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁'} (q : p₂₀₁' = p₂₀₁) + (c : cube s₀₁₁ (q ⬝ph s₂₁₁) s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : + cube s₀₁₁ s₂₁₁ (s₁₀₁ ⬝hp q) s₁₂₁ s₁₁₀ s₁₁₂ := + by induction q; exact c + end eq diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean index b06415f3f..96c703819 100644 --- a/hott/cubical/pathover2.hlean +++ b/hott/cubical/pathover2.hlean @@ -117,6 +117,10 @@ namespace eq apply ap_compose_ap02_constant end + theorem apd_constant' {A A' : Type} {B : A' → Type} {a₁ a₂ : A} {a' : A'} (b : B a') + (p : a₁ = a₂) : apd (λx, b) p = pathover_of_eq p idp := + by induction p; reflexivity + 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 diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 328908ef6..643801194 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -10,13 +10,13 @@ open eq equiv is_equiv sigma namespace eq - variables {A B : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} + variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ - + {b : B} {c : C} inductive square {A : Type} {a₀₀ : A} : Π{a₂₀ a₀₂ a₂₂ : A}, a₀₀ = a₂₀ → a₀₂ = a₂₂ → a₀₀ = a₀₂ → a₂₀ = a₂₂ → Type := @@ -633,4 +633,93 @@ namespace eq induction q, esimp at r, induction r using idp_rec_on, exact hrfl end + /- some higher coherence conditions -/ + + + theorem whisker_bl_whisker_tl_eq (p : a = a') + : whisker_bl p (whisker_tl p ids) = con.right_inv p ⬝ph vrfl := + by induction p; reflexivity + + theorem ap_is_constant_natural_square {g : B → C} {f : A → B} (H : Πa, g (f a) = c) (p : a = a') : + (ap_is_constant H p)⁻¹ ⬝ph natural_square H p ⬝hp ap_constant p c = + whisker_bl (H a') (whisker_tl (H a) ids) := + begin induction p, esimp, rewrite inv_inv, rewrite whisker_bl_whisker_tl_eq end + + definition inv_ph_eq_of_eq_ph {p : a₀₀ = a₀₂} {r : p₀₁ = p} {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} + {s₁₁' : square p₁₀ p₁₂ p p₂₁} (t : s₁₁ = r ⬝ph s₁₁') : r⁻¹ ⬝ph s₁₁ = s₁₁' := + by induction r; exact t + + -- the following is used for torus.elim_surf + theorem whisker_square_aps_eq {f : A → B} + {q₁₀ : f a₀₀ = f a₂₀} {q₀₁ : f a₀₀ = f a₀₂} {q₂₁ : f a₂₀ = f a₂₂} {q₁₂ : f a₀₂ = f a₂₂} + {r₁₀ : ap f p₁₀ = q₁₀} {r₀₁ : ap f p₀₁ = q₀₁} {r₂₁ : ap f p₂₁ = q₂₁} {r₁₂ : ap f p₁₂ = q₁₂} + {s₁₁ : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} {t₁₁ : square q₁₀ q₁₂ q₀₁ q₂₁} + (u : square (ap02 f s₁₁) (eq_of_square t₁₁) + (ap_con f p₁₀ p₂₁ ⬝ (r₁₀ ◾ r₂₁)) (ap_con f p₀₁ p₁₂ ⬝ (r₀₁ ◾ r₁₂))) + : whisker_square r₁₀ r₁₂ r₀₁ r₂₁ (aps f (square_of_eq s₁₁)) = t₁₁ := + begin + 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, + exact (eq_bot_of_square u)⁻¹ + end + + definition natural_square_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 + + definition eq_of_square_hrfl_hconcat_eq {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') + : eq_of_square (hrfl ⬝hp q⁻¹) = !idp_con ⬝ q := + by induction q; induction p; reflexivity + + definition aps_vrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : + aps f (vrefl p) = vrefl (ap f p) := + by induction p; reflexivity + + definition aps_hrfl {A B : Type} {a a' : A} (f : A → B) (p : a = a') : + aps f (hrefl p) = hrefl (ap f p) := + by induction p; reflexivity + + -- should the following two equalities be cubes? + definition natural_square_ap_fn {A B C : Type} {a a' : A} {g h : A → B} (f : B → C) (p : g ~ h) + (q : a = a') : natural_square (λa, ap f (p a)) q = + ap_compose f g q ⬝ph (aps f (natural_square p q) ⬝hp (ap_compose f h q)⁻¹) := + begin + induction q, exact !aps_vrfl⁻¹ + end + + definition natural_square_compose {A B C : Type} {a a' : A} {g g' : B → C} + (p : g ~ g') (f : A → B) (q : a = a') : natural_square (λa, p (f a)) q = + ap_compose g f q ⬝ph (natural_square p (ap f q) ⬝hp (ap_compose g' f q)⁻¹) := + by induction q; reflexivity + + definition natural_square_eq2 {A B : Type} {a a' : A} {f f' : A → B} (p : f ~ f') {q q' : a = a'} + (r : q = q') : natural_square p q = ap02 f r ⬝ph (natural_square p q' ⬝hp (ap02 f' r)⁻¹) := + by induction r; reflexivity + + definition natural_square_refl {A B : Type} {a a' : A} (f : A → B) (q : a = a') + : natural_square (homotopy.refl f) q = hrfl := + by induction q; reflexivity + + definition aps_eq_hconcat {p₀₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : + aps f (q ⬝ph s₁₁) = ap02 f q ⬝ph aps f s₁₁ := + by induction q; reflexivity + + definition aps_hconcat_eq {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁' = p₂₁) : + aps f (s₁₁ ⬝hp r⁻¹) = aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := + by induction r; reflexivity + + definition aps_hconcat_eq' {p₂₁'} (f : A → B) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p₂₁') : + aps f (s₁₁ ⬝hp r) = aps f s₁₁ ⬝hp ap02 f r := + by induction r; reflexivity + + definition aps_square_of_eq (f : A → B) (s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : + aps f (square_of_eq s) = square_of_eq ((ap_con f p₁₀ p₂₁)⁻¹ ⬝ ap02 f s ⬝ ap_con f p₀₁ p₁₂) := + by induction p₁₂; esimp at *; induction s; induction p₂₁; induction p₁₀; reflexivity + + definition aps_eq_hconcat_eq {p₀₁' p₂₁'} (f : A → B) (q : p₀₁' = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) + (r : p₂₁' = p₂₁) : aps f (q ⬝ph s₁₁ ⬝hp r⁻¹) = ap02 f q ⬝ph aps f s₁₁ ⬝hp (ap02 f r)⁻¹ := + by induction q; induction r; reflexivity + end eq diff --git a/hott/cubical/square2.hlean b/hott/cubical/square2.hlean deleted file mode 100644 index fbed9b849..000000000 --- a/hott/cubical/square2.hlean +++ /dev/null @@ -1,52 +0,0 @@ -/- -Copyright (c) 2015 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn - -Coherence conditions for operations on squares --/ - -import .square - -open equiv - -namespace eq - - variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A} - {f : A → B} {b : B} {c : C} - /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/ - {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂} - /-a₀₂-/ {p₁₂ p₁₂' : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/ - {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄} - /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/ - - theorem whisker_bl_whisker_tl_eq (p : a = a') - : whisker_bl p (whisker_tl p ids) = con.right_inv p ⬝ph vrfl := - by induction p; reflexivity - - theorem ap_is_constant_natural_square {g : B → C} {f : A → B} (H : Πa, g (f a) = c) (p : a = a') : - (ap_is_constant H p)⁻¹ ⬝ph natural_square H p ⬝hp ap_constant p c = - whisker_bl (H a') (whisker_tl (H a) ids) := - begin induction p, esimp, rewrite inv_inv, rewrite whisker_bl_whisker_tl_eq end - - definition inv_ph_eq_of_eq_ph {p : a₀₀ = a₀₂} {r : p₀₁ = p} {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} - {s₁₁' : square p₁₀ p₁₂ p p₂₁} (t : s₁₁ = r ⬝ph s₁₁') : r⁻¹ ⬝ph s₁₁ = s₁₁' := - by induction r; exact t - - -- the following is used for torus.elim_surf - theorem whisker_square_aps_eq - {q₁₀ : f a₀₀ = f a₂₀} {q₀₁ : f a₀₀ = f a₀₂} {q₂₁ : f a₂₀ = f a₂₂} {q₁₂ : f a₀₂ = f a₂₂} - {r₁₀ : ap f p₁₀ = q₁₀} {r₀₁ : ap f p₀₁ = q₀₁} {r₂₁ : ap f p₂₁ = q₂₁} {r₁₂ : ap f p₁₂ = q₁₂} - {s₁₁ : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂} {t₁₁ : square q₁₀ q₁₂ q₀₁ q₂₁} - (u : square (ap02 f s₁₁) (eq_of_square t₁₁) - (ap_con f p₁₀ p₂₁ ⬝ (r₁₀ ◾ r₂₁)) (ap_con f p₀₁ p₁₂ ⬝ (r₀₁ ◾ r₁₂))) - : whisker_square r₁₀ r₁₂ r₀₁ r₂₁ (aps f (square_of_eq s₁₁)) = t₁₁ := - begin - 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, - exact (eq_bot_of_square u)⁻¹ - end - -end eq diff --git a/hott/eq2.hlean b/hott/eq2.hlean index e3d239c09..975344cc9 100644 --- a/hott/eq2.hlean +++ b/hott/eq2.hlean @@ -6,8 +6,8 @@ Author: Floris van Doorn Theorems about 2-dimensional paths -/ -import .cubical.square -open function +import .cubical.square .function +open function is_equiv equiv namespace eq variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B} @@ -141,4 +141,118 @@ namespace eq : whisker_left p q⁻² ⬝ q = con.right_inv p := by cases q; reflexivity + definition cast_fn_cast_square {A : Type} {B C : A → Type} (f : Π⦃a⦄, B a → C a) {a₁ a₂ : A} + (p : a₁ = a₂) (q : a₂ = a₁) (r : p ⬝ q = idp) (b : B a₁) : + cast (ap C q) (f (cast (ap B p) b)) = f b := + have q⁻¹ = p, from inv_eq_of_idp_eq_con r⁻¹, + begin induction this, induction q, reflexivity end + + definition ap011_ap_square_right {A B C : Type} (f : A → B → C) {a a' : A} (p : a = a') + {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : + square (ap011 f p q₁₂) (ap (λx, f x b₃) p) (ap (f a) q₁₃) (ap (f a') q₂₃) := + by induction r; induction q₂₃; induction q₁₂; induction p; exact ids + + definition ap011_ap_square_left {A B C : Type} (f : B → A → C) {a a' : A} (p : a = a') + {b₁ b₂ b₃ : B} {q₁₂ : b₁ = b₂} {q₂₃ : b₂ = b₃} {q₁₃ : b₁ = b₃} (r : q₁₂ ⬝ q₂₃ = q₁₃) : + square (ap011 f q₁₂ p) (ap (f b₃) p) (ap (λx, f x a) q₁₃) (ap (λx, f x a') q₂₃) := + by induction r; induction q₂₃; induction q₁₂; induction p; exact ids + + definition con2_assoc {A : Type} {x y z t : A} {p p' : x = y} {q q' : y = z} {r r' : z = t} + (h : p = p') (h' : q = q') (h'' : r = r') : + square ((h ◾ h') ◾ h'') (h ◾ (h' ◾ h'')) (con.assoc p q r) (con.assoc p' q' r') := + by induction h; induction h'; induction h''; exact hrfl + + definition con_left_inv_idp {A : Type} {x : A} {p : x = x} (q : p = idp) + : con.left_inv p = q⁻² ◾ q := + by cases q; reflexivity + + definition eckmann_hilton_con2 {A : Type} {x : A} {p p' q q': idp = idp :> x = x} + (h : p = p') (h' : q = q') : square (h ◾ h') (h' ◾ h) (eckmann_hilton p q) (eckmann_hilton p' q') := + by induction h; induction h'; exact hrfl + + definition ap_con_fn {A B : Type} {a a' : A} {b : B} (g h : A → b = b) (p : a = a') : + ap (λa, g a ⬝ h a) p = ap g p ◾ ap h p := + by induction p; reflexivity + + definition ap_eq_ap011 {A B C X : Type} (f : A → B → C) (g : X → A) (h : X → B) {x x' : X} + (p : x = x') : ap (λx, f (g x) (h x)) p = ap011 f (ap g p) (ap h p) := + by induction p; reflexivity + + definition ap_is_weakly_constant {A B : Type} {f : A → B} + (h : is_weakly_constant f) {a a' : A} (p : a = a') : ap f p = (h a a)⁻¹ ⬝ h a a' := + by induction p; exact !con.left_inv⁻¹ + + definition ap_is_constant_idp {A B : Type} {f : A → B} {b : B} (p : Πa, f a = b) {a : A} (q : a = a) + (r : q = idp) : ap_is_constant p q = ap02 f r ⬝ (con.right_inv (p a))⁻¹ := + by cases r; exact !idp_con⁻¹ + + definition con_right_inv_natural {A : Type} {a a' : A} {p p' : a = a'} (q : p = p') : + con.right_inv p = q ◾ q⁻² ⬝ con.right_inv p' := + by induction q; induction p; reflexivity + + definition whisker_right_ap {A B : Type} {a a' : A}{b₁ b₂ b₃ : B} (q : b₂ = b₃) (f : A → b₁ = b₂) + (p : a = a') : whisker_right q (ap f p) = ap (λa, f a ⬝ q) p := + by induction p; reflexivity + + definition ap02_ap_constant {A B C : Type} {a a' : A} (f : B → C) (b : B) (p : a = a') : + square (ap_constant p (f b)) (ap02 f (ap_constant p b)) (ap_compose f (λx, b) p) idp := + by induction p; exact ids + + definition ap_constant_compose {A B C : Type} {a a' : A} (c : C) (f : A → B) (p : a = a') : + square (ap_constant p c) (ap_constant (ap f p) c) (ap_compose (λx, c) f p) idp := + by induction p; exact ids + + definition ap02_constant {A B : Type} {a a' : A} (b : B) {p p' : a = a'} + (q : p = p') : square (ap_constant p b) (ap_constant p' b) (ap02 (λx, b) q) idp := + by induction q; exact vrfl + + section hsquare + variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type} + {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀} + {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂} {f₄₁ : A₄₀ → A₄₂} + {f₁₂ : A₀₂ → A₂₂} {f₃₂ : A₂₂ → A₄₂} + {f₀₃ : A₀₂ → A₀₄} {f₂₃ : A₂₂ → A₂₄} {f₄₃ : A₄₂ → A₄₄} + {f₁₄ : A₀₄ → A₂₄} {f₃₄ : A₂₄ → A₄₄} + + definition hsquare [reducible] (f₁₀ : A₀₀ → A₂₀) (f₁₂ : A₀₂ → A₂₂) + (f₀₁ : A₀₀ → A₀₂) (f₂₁ : A₂₀ → A₂₂) : Type := + f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ + + definition hsquare_of_homotopy (p : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁) : hsquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition homotopy_of_hsquare (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘ f₁₀ ~ f₁₂ ∘ f₀₁ := + p + + definition homotopy_top_of_hsquare {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + + definition homotopy_top_of_hsquare' [is_equiv f₂₁] (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + f₁₀ ~ f₂₁⁻¹ ∘ f₁₂ ∘ f₀₁ := + homotopy_inv_of_homotopy_post _ _ _ p + + definition hhconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₃₀ f₃₂ f₂₁ f₄₁) : + hsquare (f₃₀ ∘ f₁₀) (f₃₂ ∘ f₁₂) f₀₁ f₄₁ := + hwhisker_right f₁₀ q ⬝hty hwhisker_left f₃₂ p + + definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) : + hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) := + (hhconcat p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ + + definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ := + λb, eq_inv_of_eq ((p (f₁₀⁻¹ᵉ b))⁻¹ ⬝ ap f₂₁ (to_right_inv f₁₀ b)) + + definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) : + hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ := + (hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ + + infix ` ⬝htyh `:73 := hhconcat + infix ` ⬝htyv `:73 := hvconcat + postfix `⁻¹ʰᵗʸʰ`:(max+1) := hhinverse + postfix `⁻¹ʰᵗʸᵛ`:(max+1) := hvinverse + + end hsquare + end eq diff --git a/hott/function.hlean b/hott/function.hlean index 9d3440fac..a63df8e54 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -7,24 +7,18 @@ Ported from Coq HoTT Theorems about embeddings and surjections -/ -import hit.trunc types.equiv cubical.square +import hit.trunc types.equiv cubical.square types.nat -open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod +open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod pointed nat -variables {A B C : Type} (f : A → B) {b : B} +variables {A B C : Type} (f f' : A → B) {b : B} /- the image of a map is the (-1)-truncated fiber -/ definition image' [constructor] (f : A → B) (b : B) : Type := ∥ fiber f b ∥ definition is_prop_image' [instance] (f : A → B) (b : B) : is_prop (image' f b) := !is_trunc_trunc definition image [constructor] (f : A → B) (b : B) : Prop := Prop.mk (image' f b) _ -definition image.mk [constructor] {f : A → B} {b : B} (a : A) (p : f a = b) - : image f b := -tr (fiber.mk a p) - -protected definition image.rec [unfold 8] [recursor 8] {f : A → B} {b : B} {P : image' f b → Type} - [H : Πv, is_prop (P v)] (H : Π(a : A) (p : f a = b), P (image.mk a p)) (v : image' f b) : P v := -begin unfold [image'] at *, induction v with v, induction v with a p, exact H a p end +definition total_image {A B : Type} (f : A → B) : Type := sigma (image f) definition is_embedding [class] (f : A → B) := Π(a a' : A), is_equiv (ap f : a = a' → f a = f a') @@ -50,6 +44,33 @@ structure is_conditionally_constant [class] (f : A → B) := (g : ∥A∥ → B) (eq : Π(a : A), f a = g (tr a)) +section image +protected definition image.mk [constructor] {f : A → B} {b : B} (a : A) (p : f a = b) + : image f b := +tr (fiber.mk a p) + +protected definition image.rec [unfold 8] [recursor 8] {f : A → B} {b : B} {P : image' f b → Type} + [H : Πv, is_prop (P v)] (H : Π(a : A) (p : f a = b), P (image.mk a p)) (v : image' f b) : P v := +begin unfold [image'] at *, induction v with v, induction v with a p, exact H a p end + +definition image.elim {A B : Type} {f : A → B} {C : Type} [is_prop C] {b : B} + (H : image f b) (H' : ∀ (a : A), f a = b → C) : C := +begin + refine (trunc.elim _ H), + intro H'', cases H'' with a Ha, exact H' a Ha +end + +definition image.equiv_exists {A B : Type} {f : A → B} {b : B} : image f b ≃ ∃ a, f a = b := +trunc_equiv_trunc _ (fiber.sigma_char _ _) + +definition image_pathover {f : A → B} {x y : B} (p : x = y) (u : image f x) (v : image f y) : + u =[p] v := +!is_prop.elimo + +/- total_image.elim_set is in hit.prop_trunc to avoid dependency cycle -/ + +end image + namespace function abbreviation sect [unfold 4] := @is_retraction.sect @@ -304,6 +325,51 @@ namespace function : is_embedding (@pr1 A B) := λv v', to_is_equiv (sigma_eq_equiv v v' ⬝e !sigma_equiv_of_is_contr_right) + variables {f f'} + definition is_embedding_homotopy_closed (p : f ~ f') (H : is_embedding f) : is_embedding f' := + begin + intro a a', fapply is_equiv_of_equiv_of_homotopy, + exact equiv.mk (ap f) _ ⬝e equiv_eq_closed_left _ (p a) ⬝e equiv_eq_closed_right _ (p a'), + intro q, esimp, exact (eq_bot_of_square (transpose (natural_square p q)))⁻¹ + end + + definition is_embedding_homotopy_closed_rev (p : f' ~ f) (H : is_embedding f) : is_embedding f' := + is_embedding_homotopy_closed p⁻¹ʰᵗʸ H + + definition is_surjective_homotopy_closed (p : f ~ f') (H : is_surjective f) : is_surjective f' := + begin + intro b, induction H b with a q, + exact image.mk a ((p a)⁻¹ ⬝ q) + end + + definition is_surjective_homotopy_closed_rev (p : f' ~ f) (H : is_surjective f) : + is_surjective f' := + is_surjective_homotopy_closed p⁻¹ʰᵗʸ H + + definition is_equiv_ap1_gen_of_is_embedding {A B : Type} (f : A → B) [is_embedding f] + {a a' : A} {b b' : B} (q : f a = b) (q' : f a' = b') : is_equiv (ap1_gen f q q') := + begin + induction q, induction q', + exact is_equiv.homotopy_closed _ (ap1_gen_idp_left f)⁻¹ʰᵗʸ, + end + + definition is_equiv_ap1_of_is_embedding {A B : Type*} (f : A →* B) [is_embedding f] : + is_equiv (Ω→ f) := + is_equiv_ap1_gen_of_is_embedding f (respect_pt f) (respect_pt f) + + definition loop_pequiv_loop_of_is_embedding [constructor] {A B : Type*} (f : A →* B) + [is_embedding f] : Ω A ≃* Ω B := + pequiv_of_pmap (Ω→ f) (is_equiv_ap1_of_is_embedding f) + + definition loopn_pequiv_loopn_of_is_embedding [constructor] (n : ℕ) [H : is_succ n] + {A B : Type*} (f : A →* B) [is_embedding f] : Ω[n] A ≃* Ω[n] B := + begin + induction H with n, + exact !loopn_succ_in ⬝e* + loopn_pequiv_loopn n (loop_pequiv_loop_of_is_embedding f) ⬝e* + !loopn_succ_in⁻¹ᵉ* + end + /- The definitions is_surjective_of_is_equiv diff --git a/hott/hit/prop_trunc.hlean b/hott/hit/prop_trunc.hlean index a4ff4c302..092fdaa56 100644 --- a/hott/hit/prop_trunc.hlean +++ b/hott/hit/prop_trunc.hlean @@ -1,4 +1,4 @@ -import function types.trunc hit.colimit homotopy.connectedness --types.nat.hott hit.trunc cubical.square +import types.trunc hit.colimit homotopy.connectedness open eq is_trunc unit quotient seq_colim pi nat equiv sum algebra is_conn function @@ -409,7 +409,7 @@ open prop_trunc trunc -- Corollaries for the actual truncation. namespace is_trunc local attribute is_prop_trunc_one_step_tr [instance] - definition is_prop.elim_set {A : Type} {P : Type} [is_set P] (f : A → P) + definition prop_trunc.elim_set [unfold 6] {A : Type} {P : Type} [is_set P] (f : A → P) (p : Πa a', f a = f a') (x : trunc -1 A) : P := begin have y : trunc 0 (one_step_tr A), @@ -420,8 +420,32 @@ namespace is_trunc { exact p a a'} end - definition is_prop.elim_set_tr {A : Type} {P : Type} {H : is_set P} (f : A → P) - (p : Πa a', f a = f a') (a : A) : is_prop.elim_set f p (tr a) = f a := + definition prop_trunc.elim_set_tr {A : Type} {P : Type} {H : is_set P} (f : A → P) + (p : Πa a', f a = f a') (a : A) : prop_trunc.elim_set f p (tr a) = f a := by reflexivity + open sigma + + local attribute prop_trunc.elim_set [recursor 6] + definition total_image.elim_set [unfold 8] + {A B : Type} {f : A → B} {C : Type} [is_set C] + (g : A → C) (h : Πa a', f a = f a' → g a = g a') (x : total_image f) : C := + begin + induction x with b v, + induction v using prop_trunc.elim_set with x x x', + { induction x with a p, exact g a }, + { induction x with a p, induction x' with a' p', induction p', exact h _ _ p } + end + + definition total_image.rec [unfold 7] + {A B : Type} {f : A → B} {C : total_image f → Type} [H : Πx, is_prop (C x)] + (g : Πa, C ⟨f a, image.mk a idp⟩) + (x : total_image f) : C x := + begin + induction x with b v, + refine @image.rec _ _ _ _ _ (λv, H ⟨b, v⟩) _ v, + intro a p, + induction p, exact g a + end + end is_trunc diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index fc99321ed..56525a1d1 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -112,6 +112,16 @@ namespace pushout variables {TL BL TR : Type} (f : TL → BL) (g : TL → TR) + protected theorem elim_inl {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : BL} (p : b = b') + : ap (pushout.elim Pinl Pinr Pglue) (ap inl p) = ap Pinl p := + !ap_compose⁻¹ + + protected theorem elim_inr {P : Type} (Pinl : BL → P) (Pinr : TR → P) + (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) {b b' : TR} (p : b = b') + : ap (pushout.elim Pinl Pinr Pglue) (ap inr p) = ap Pinr p := + !ap_compose⁻¹ + /- The non-dependent universal property -/ definition pushout_arrow_equiv (C : Type) : (pushout f g → C) ≃ (Σ(i : BL → C) (j : TR → C), Πc, i (f c) = j (g c)) := diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean index 9f1cdf570..b8a68e7c6 100644 --- a/hott/hit/set_quotient.hlean +++ b/hott/hit/set_quotient.hlean @@ -8,7 +8,7 @@ Declaration of set-quotients, i.e. quotient of a mere relation which is then set import function algebra.relation types.trunc types.eq hit.quotient -open eq is_trunc trunc quotient equiv +open eq is_trunc trunc quotient equiv is_equiv namespace set_quotient section @@ -86,6 +86,36 @@ namespace set_quotient definition is_surjective_class_of : is_surjective (class_of : A → set_quotient R) := λx, set_quotient.rec_on x (λa, tr (fiber.mk a idp)) (λa a' r, !is_prop.elimo) + definition is_prop_set_quotient {A : Type} (R : A → A → Prop) [is_prop A] : + is_prop (set_quotient R) := + begin + apply is_prop.mk, intro x y, + induction x using set_quotient.rec_prop, induction y using set_quotient.rec_prop, + exact ap class_of !is_prop.elim + end + + local attribute is_prop_set_quotient [instance] + definition is_trunc_set_quotient [instance] (n : ℕ₋₂) {A : Type} (R : A → A → Prop) [is_trunc n A] : + is_trunc n (set_quotient R) := + begin + cases n with n, { apply is_contr_of_inhabited_prop, exact class_of !center }, + cases n with n, { apply _ }, + apply is_trunc_succ_succ_of_is_set + end + + definition is_equiv_class_of [constructor] {A : Type} [is_set A] (R : A → A → Prop) + (p : Π⦃a b⦄, R a b → a = b) : is_equiv (@class_of A R) := + begin + fapply adjointify, + { intro x, induction x, exact a, exact p H }, + { intro x, induction x using set_quotient.rec_prop, reflexivity }, + { intro a, reflexivity } + end + + definition equiv_set_quotient [constructor] {A : Type} [is_set A] (R : A → A → Prop) + (p : Π⦃a b⦄, R a b → a = b) : A ≃ set_quotient R := + equiv.mk _ (is_equiv_class_of R p) + /- non-dependent universal property -/ definition set_quotient_arrow_equiv (B : Type) [H : is_set B] : diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 992b527d0..8d02dc9fb 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -126,6 +126,10 @@ namespace trunc definition or.intro_left [reducible] [constructor] (x : X) : X ∨ Y := tr (inl x) definition or.intro_right [reducible] [constructor] (y : Y) : X ∨ Y := tr (inr y) + definition exists.elim {A : Type} {p : A → Type} {B : Type} [is_prop B] (H : Exists p) + (H' : ∀ (a : A), p a → B) : B := + trunc.elim (sigma.rec H') H + definition is_contr_of_merely_prop [H : is_prop A] (aa : merely A) : is_contr A := is_contr_of_inhabited_prop (trunc.rec_on aa id) diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean index 352031bf8..0aacd9e55 100644 --- a/hott/hit/two_quotient.hlean +++ b/hott/hit/two_quotient.hlean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube cubical.square2 +import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube open quotient eq circle sum sigma equiv function relation e_closure diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index e1f3d37b1..e75092eba 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -353,4 +353,27 @@ namespace circle definition circle_base_mul [reducible] (x : S¹) : circle_mul base x = x := idp + /- + Suppose for `f, g : A -> B` we 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 ap square_of_pathover !rec_loop ⬝ _, + exact to_right_inv !eq_pathover_equiv_square q + end + + definition circle_elim_constant [unfold 5] {A : Type} {a : A} {p : a = a} (r : p = idp) (x : S¹) : + circle.elim a p x = a := + begin + induction x, + { reflexivity }, + { apply eq_pathover_constant_right, apply hdeg_square, exact !elim_loop ⬝ r } + end + end circle diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index f25d4a71b..00e4fdabb 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -112,7 +112,7 @@ namespace is_conn apply eq_equiv_eq_symm end, apply @is_trunc_equiv_closed _ _ k e, clear e, - apply IH (λb : B, (g b = h b)) (λb, @is_trunc_eq (P b) (n +2+ k) (HP b) (g b) (h b))} + apply IH (λb : B, (g b = h b)) (λb, @is_trunc_eq (P b) (n +2+ k) (HP b) (g b) (h b)) } end end @@ -365,6 +365,101 @@ namespace is_conn rewrite -of_nat_add_two, exact _ end + definition is_conn_equiv_closed_rev (n : ℕ₋₂) {A B : Type} (f : A ≃ B) (H : is_conn n B) : + is_conn n A := + is_conn_equiv_closed n f⁻¹ᵉ _ + + definition is_conn_succ_intro {n : ℕ₋₂} {A : Type} (a : trunc (n.+1) A) + (H2 : Π(a a' : A), is_conn n (a = a')) : is_conn (n.+1) A := + begin + apply @is_contr_of_inhabited_prop, + { apply is_trunc_succ_intro, + refine trunc.rec _, intro a, refine trunc.rec _, intro a', + apply is_contr_equiv_closed !tr_eq_tr_equiv⁻¹ᵉ }, + exact a + end + + definition is_conn_pathover (n : ℕ₋₂) {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a) + (b' : B a') [is_conn (n.+1) (B a')] : is_conn n (b =[p] b') := + is_conn_equiv_closed_rev n !pathover_equiv_tr_eq _ + + open sigma + lemma is_conn_sigma [instance] {A : Type} (B : A → Type) (n : ℕ₋₂) + [HA : is_conn n A] [HB : Πa, is_conn n (B a)] : is_conn n (Σa, B a) := + begin + revert A B HA HB, induction n with n IH: intro A B HA HB, + { apply is_conn_minus_two }, + apply is_conn_succ_intro, + { induction center (trunc (n.+1) A) with a, induction center (trunc (n.+1) (B a)) with b, + exact tr ⟨a, b⟩ }, + intro a a', refine is_conn_equiv_closed_rev n !sigma_eq_equiv _, + apply IH, apply is_conn_eq, intro p, apply is_conn_pathover + /- an alternative proof of the successor case -/ + -- induction center (trunc (n.+1) A) with a₀, + -- induction center (trunc (n.+1) (B a₀)) with b₀, + -- apply is_contr.mk (tr ⟨a₀, b₀⟩), + -- intro ab, induction ab with ab, induction ab with a b, + -- induction tr_eq_tr_equiv n a₀ a !is_prop.elim with p, induction p, + -- induction tr_eq_tr_equiv n b₀ b !is_prop.elim with q, induction q, + -- reflexivity + end + + lemma is_conn_prod [instance] (A B : Type) (n : ℕ₋₂) [is_conn n A] [is_conn n B] : + is_conn n (A × B) := + is_conn_equiv_closed n !sigma.equiv_prod _ + + lemma is_conn_fun_of_is_conn {A B : Type} (n : ℕ₋₂) (f : A → B) + [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn_fun n f := + λb, is_conn_equiv_closed_rev n !fiber.sigma_char _ + + lemma is_conn_pfiber {A B : Type*} (n : ℕ₋₂) (f : A →* B) + [HA : is_conn n A] [HB : is_conn (n.+1) B] : is_conn n (pfiber f) := + is_conn_fun_of_is_conn n f pt + + definition is_conn_fun_trunc_elim_of_le {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) + (H : k ≤ n) [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := + begin + apply is_conn_fun.intro, + intro P, have Πb, is_trunc n (P b), from (λb, is_trunc_of_le _ H), + fconstructor, + { intro f' b, + refine is_conn_fun.elim k H2 _ _ b, intro a, exact f' (tr a) }, + { intro f', apply eq_of_homotopy, intro a, + induction a with a, esimp, rewrite [is_conn_fun.elim_β] } + end + + definition is_conn_fun_trunc_elim_of_ge {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) + (H : n ≤ k) [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := + 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, + apply is_equiv_of_equiv_of_homotopy (equiv.mk (trunc_functor n f) _ ⬝e !trunc_equiv), + intro x, induction x, reflexivity + end + + definition is_conn_fun_trunc_elim {n k : ℕ₋₂} {A B : Type} [is_trunc n B] (f : A → B) + [H2 : is_conn_fun k f] : is_conn_fun k (trunc.elim f : trunc n A → B) := + begin + eapply algebra.le_by_cases k n: intro H, + { exact is_conn_fun_trunc_elim_of_le f H }, + { exact is_conn_fun_trunc_elim_of_ge f H } + end + + lemma is_conn_fun_tr (n : ℕ₋₂) (A : Type) : is_conn_fun n (tr : A → trunc n A) := + begin + apply is_conn_fun.intro, + intro P, + fconstructor, + { intro f' b, induction b with a, exact f' a }, + { intro f', reflexivity } + end + + + definition is_contr_of_is_conn_of_is_trunc {n : ℕ₋₂} {A : Type} (H : is_trunc n A) + (K : is_conn n A) : is_contr A := + is_contr_equiv_closed (trunc_equiv n A) + end is_conn /- diff --git a/hott/homotopy/homotopy_group.hlean b/hott/homotopy/homotopy_group.hlean index 673260167..3939f6695 100644 --- a/hott/homotopy/homotopy_group.hlean +++ b/hott/homotopy/homotopy_group.hlean @@ -223,6 +223,52 @@ namespace is_trunc cases A with A a, exact H k H' end + + + definition ab_group_homotopy_group_of_is_conn (n : ℕ) (A : Type*) [H : is_conn 1 A] : + ab_group (π[n] A) := + begin + have is_conn 0 A, from !is_conn_of_is_conn_succ, + cases n with n, + { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, + cases n with n, + { unfold [homotopy_group, ptrunc], apply ab_group_of_is_contr }, + exact ab_group_homotopy_group n A + end + + definition is_contr_of_trivial_homotopy' (n : ℕ₋₂) (A : Type) [is_trunc n A] [is_conn -1 A] + (H : Πk a, is_contr (π[k] (pointed.MK A a))) : is_contr A := + begin + assert aa : trunc -1 A, + { apply center }, + assert H3 : is_conn 0 A, + { induction aa with a, exact H 0 a }, + exact is_contr_of_trivial_homotopy n A H + end + + definition is_conn_of_trivial_homotopy (n : ℕ₋₂) (m : ℕ) (A : Type) [is_trunc n A] [is_conn 0 A] + (H : Π(k : ℕ) a, k ≤ m → is_contr (π[k] (pointed.MK A a))) : is_conn m A := + begin + apply is_contr_of_trivial_homotopy_nat m (trunc m A), + intro k a H2, + induction a with a, + apply is_trunc_equiv_closed_rev, + exact equiv_of_pequiv (homotopy_group_trunc_of_le (pointed.MK A a) _ _ H2), + exact H k a H2 + end + + definition is_conn_of_trivial_homotopy_pointed (n : ℕ₋₂) (m : ℕ) (A : Type*) [is_trunc n A] + (H : Π(k : ℕ), k ≤ m → is_contr (π[k] A)) : is_conn m A := + begin + have is_conn 0 A, proof H 0 !zero_le qed, + apply is_conn_of_trivial_homotopy n m A, + intro k a H2, revert a, apply is_conn.elim -1, + cases A with A a, exact H k H2 + end + + + + definition is_conn_fun_of_equiv_on_homotopy_groups.{u} (n : ℕ) {A B : Type.{u}} (f : A → B) [is_equiv (trunc_functor 0 f)] (H1 : Πa k, k ≤ n → is_equiv (homotopy_group_functor k (pmap_of_map f a))) diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 94d4de7d2..391a5ad21 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -302,10 +302,17 @@ namespace sphere definition sphere_eq_pbool : S* 0 = pbool := pType_eq sphere_equiv_bool idp + definition psphere_pequiv_iterate_psusp (n : ℕ) : psphere n ≃* iterate_psusp n pbool := + begin + induction n with n e, + { exact psphere_pequiv_pbool }, + { exact psusp_pequiv e } + end + definition psphere_pmap_pequiv' (A : Type*) (n : ℕ) : ppmap (S* n) A ≃* Ω[n] A := begin revert A, induction n with n IH: intro A, - { refine _ ⬝e* !pmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* }, + { refine _ ⬝e* !ppmap_pbool_pequiv, exact pequiv_ppcompose_right psphere_pequiv_pbool⁻¹ᵉ* }, { refine psusp_adjoint_loop (S* n) A ⬝e* IH (Ω A) ⬝e* !loopn_succ_in⁻¹ᵉ* } end diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 43c873417..e998bb161 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -226,20 +226,43 @@ namespace susp definition psusp_pequiv [constructor] (f : X ≃* Y) : psusp X ≃* psusp Y := pequiv_of_equiv (susp.equiv f) idp - definition psusp_functor_compose (g : Y →* Z) (f : X →* Y) - : psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f := + definition psusp_functor_pcompose (g : Y →* Z) (f : X →* Y) : + psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f := begin - fconstructor, - { intro a, induction a, + fapply phomotopy.mk, + { intro x, induction x, { reflexivity }, { reflexivity }, - { apply eq_pathover, apply hdeg_square, - rewrite [▸*,ap_compose' _ (psusp_functor f)], - krewrite +susp.elim_merid } }, - { reflexivity } + { apply eq_pathover, apply hdeg_square, esimp, + refine !elim_merid ⬝ _ ⬝ (ap_compose (psusp_functor g) _ _)⁻¹ᵖ, + refine _ ⬝ ap02 _ !elim_merid⁻¹, exact !elim_merid⁻¹ }}, + { reflexivity }, end - -- adjunction from Coq-HoTT + definition psusp_functor_phomotopy {f g : X →* Y} (p : f ~* g) : + psusp_functor f ~* psusp_functor g := + begin + fapply phomotopy.mk, + { intro x, induction x, + { reflexivity }, + { reflexivity }, + { apply eq_pathover, apply hdeg_square, esimp, refine !elim_merid ⬝ _ ⬝ !elim_merid⁻¹ᵖ, + exact ap merid (p a), }}, + { reflexivity }, + end + + definition psusp_functor_pid (A : Type*) : psusp_functor (pid A) ~* pid (psusp A) := + begin + fapply phomotopy.mk, + { intro x, induction x, + { reflexivity }, + { reflexivity }, + { apply eq_pathover_id_right, apply hdeg_square, apply elim_merid }}, + { reflexivity }, + end + + /- adjunction originally ported from Coq-HoTT, + but we proved some additional naturality conditions -/ definition loop_psusp_unit [constructor] (X : Type*) : X →* Ω(psusp X) := begin @@ -324,6 +347,28 @@ namespace susp definition loop_psusp_intro [constructor] {X Y : Type*} (f : psusp X →* Y) : X →* Ω Y := ap1 f ∘* loop_psusp_unit X + definition psusp_elim_psusp_functor {A B C : Type*} (g : B →* Ω C) (f : A →* B) : + psusp.elim g ∘* psusp_functor f ~* psusp.elim (g ∘* f) := + begin + refine !passoc ⬝* _, exact pwhisker_left _ !psusp_functor_pcompose⁻¹* + end + + definition psusp_elim_phomotopy {A B : Type*} {f g : A →* Ω B} (p : f ~* g) : psusp.elim f ~* psusp.elim g := + pwhisker_left _ (psusp_functor_phomotopy p) + + definition psusp_elim_natural {X Y Z : Type*} (g : Y →* Z) (f : X →* Ω Y) + : g ∘* psusp.elim f ~* psusp.elim (Ω→ g ∘* f) := + begin + refine _ ⬝* pwhisker_left _ !psusp_functor_pcompose⁻¹*, + refine !passoc⁻¹* ⬝* _ ⬝* !passoc, + exact pwhisker_right _ !loop_psusp_counit_natural + end + + definition loop_psusp_intro_natural {X Y Z : Type*} (g : psusp Y →* Z) (f : X →* Y) : + loop_psusp_intro (g ∘* psusp_functor f) ~* loop_psusp_intro g ∘* f := + pwhisker_right _ !ap1_pcompose ⬝* !passoc ⬝* pwhisker_left _ !loop_psusp_unit_natural⁻¹* ⬝* + !passoc⁻¹* + definition psusp_adjoint_loop_right_inv {X Y : Type*} (g : X →* Ω Y) : loop_psusp_intro (psusp.elim g) ~* g := begin @@ -338,7 +383,7 @@ namespace susp definition psusp_adjoint_loop_left_inv {X Y : Type*} (f : psusp X →* Y) : psusp.elim (loop_psusp_intro f) ~* f := begin - refine !pwhisker_left !psusp_functor_compose ⬝* _, + refine !pwhisker_left !psusp_functor_pcompose ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !loop_psusp_counit_natural⁻¹* ⬝* _, refine !passoc ⬝* _, @@ -388,7 +433,7 @@ namespace susp esimp [psusp_adjoint_loop], refine _ ⬝* !passoc⁻¹*, apply pwhisker_left, - apply psusp_functor_compose + apply psusp_functor_pcompose end /- iterated suspension -/ @@ -442,4 +487,6 @@ namespace susp symmetry, apply loopn_succ_in } end + + end susp diff --git a/hott/homotopy/vankampen.hlean b/hott/homotopy/vankampen.hlean index 759d9a6ca..71dd38508 100644 --- a/hott/homotopy/vankampen.hlean +++ b/hott/homotopy/vankampen.hlean @@ -59,7 +59,7 @@ namespace pushout protected definition code_equiv (x : BL + TR) (y : TL) : @hom C _ x (sum.inl (f y)) ≃ @hom C _ x (sum.inr (g y)) := begin - refine @is_prop.elim_set _ _ _ _ _ (ksurj y), { apply @is_trunc_equiv: apply is_set_hom}, + refine @prop_trunc.elim_set _ _ _ _ _ (ksurj y), { apply @is_trunc_equiv: apply is_set_hom}, { intro v, cases v with s p, exact code_equiv_pt x p}, intro v v', cases v with s p, cases v' with s' p', @@ -74,7 +74,7 @@ namespace pushout refine @set_quotient.rec_prop _ _ _ _ _ h, {intro l, apply is_trunc_eq, apply is_set_hom}, intro l, have ksurj (k s) = tr (fiber.mk s idp), from !is_prop.elim, - refine ap (λz, to_fun (@is_prop.elim_set _ _ _ _ _ z) (class_of l)) this ⬝ _, + refine ap (λz, to_fun (@prop_trunc.elim_set _ _ _ _ _ z) (class_of l)) this ⬝ _, change class_of ([iE k F G (tr idp), DE k F G s, iD k F G (tr idp)] ++ l) = class_of (DE k F G s :: l) :> @hom C _ _ _, refine eq_of_rel (tr _) ⬝ (eq_of_rel (tr _)), diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index ba1e73490..aecdfd7db 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -16,8 +16,11 @@ infixr ` ∨ ` := pwedge namespace wedge + protected definition glue {A B : Type*} : inl pt = inr pt :> wedge A B := + pushout.glue ⋆ + protected definition rec {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) - (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) (glue ⋆) (Pinr pt)) + (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) wedge.glue (Pinr pt)) (y : wedge A B) : P y := by induction y; apply Pinl; apply Pinr; induction x; exact Pglue @@ -25,6 +28,16 @@ namespace wedge (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) (y : wedge A B) : P := by induction y with a b x; exact Pinl a; exact Pinr b; induction x; exact Pglue + protected definition rec_glue {A B : Type*} {P : wedge A B → Type} (Pinl : Π(x : A), P (inl x)) + (Pinr : Π(x : B), P (inr x)) (Pglue : pathover P (Pinl pt) wedge.glue (Pinr pt)) : + apd (wedge.rec Pinl Pinr Pglue) wedge.glue = Pglue := + !pushout.rec_glue + + protected definition elim_glue {A B : Type*} {P : Type} (Pinl : A → P) + (Pinr : B → P) (Pglue : Pinl pt = Pinr pt) : ap (wedge.elim Pinl Pinr Pglue) wedge.glue = Pglue := + !pushout.elim_glue + + end wedge attribute wedge.rec wedge.elim [recursor 7] [unfold 7] @@ -38,7 +51,7 @@ namespace wedge { fapply pmap.mk, intro a, apply pinr a, apply respect_pt }, { fapply is_equiv.adjointify, intro x, fapply pushout.elim_on x, exact λ x, Point A, exact id, intro u, reflexivity, - intro x, fapply pushout.rec_on x, intro u, cases u, esimp, apply (glue unit.star)⁻¹, + intro x, fapply pushout.rec_on x, intro u, cases u, esimp, apply wedge.glue⁻¹, intro a, reflexivity, intro u, cases u, esimp, apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, fapply eq_hconcat, apply ap_compose inr, diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 601561b59..48f936cf8 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -119,6 +119,10 @@ namespace is_equiv (λ b, ap f !Hty⁻¹ ⬝ right_inv f b) (λ a, !Hty⁻¹ ⬝ left_inv f a) + definition inv_homotopy_inv {A B : Type} {f g : A → B} [is_equiv f] [is_equiv g] (p : f ~ g) + : f⁻¹ ~ g⁻¹ := + λb, (left_inv g (f⁻¹ b))⁻¹ ⬝ ap g⁻¹ ((p (f⁻¹ b))⁻¹ ⬝ right_inv f b) + definition is_equiv_up [instance] [constructor] (A : Type) : is_equiv (up : A → lift A) := adjointify up down (λa, by induction a;reflexivity) (λa, idp) @@ -376,6 +380,9 @@ namespace equiv 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 to_inv_homotopy_inv {f g : A ≃ B} (p : f ~ g) : f⁻¹ᵉ ~ g⁻¹ᵉ := + inv_homotopy_inv p + --we need this theorem for the funext_of_ua proof theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ := eq.rec_on p idp diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 3037b04d0..64e7b0d35 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -278,6 +278,13 @@ namespace eq refine homotopy.rec_on' p _, intro q, induction q, exact H end + protected definition homotopy.rec_on_idp_left {A : Type} {P : A → Type} {g : Πa, P a} + {Q : Πf, (f ~ g) → Type} {f : Π x, P x} + (p : f ~ g) (H : Q g (homotopy.refl g)) : Q f p := + begin + induction p using homotopy.rec_on, induction q, exact H + end + definition eq_of_homotopy_inv {f g : Π x, P x} (H : f ~ g) : eq_of_homotopy (λx, (H x)⁻¹) = (eq_of_homotopy H)⁻¹ := begin diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 408db14e6..e80308050 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -67,11 +67,11 @@ namespace eq p₁ ⬝ (p₂ ⬝ p₃ ⬝ p₄) ⬝ p₅ = (p₁ ⬝ p₂) ⬝ p₃ ⬝ (p₄ ⬝ p₅) := by induction p₅; induction p₄; induction p₃; reflexivity - -- The left inverse law. + -- The right inverse law. definition con.right_inv [unfold 4] (p : x = y) : p ⬝ p⁻¹ = idp := by induction p; reflexivity - -- The right inverse law. + -- The left inverse law. definition con.left_inv [unfold 4] (p : x = y) : p⁻¹ ⬝ p = idp := by induction p; reflexivity @@ -112,6 +112,12 @@ namespace eq (H₁ : a = b) (H₂ : C (H₁⁻¹⁻¹)) : C H₁ := eq.rec_on (inv_inv H₁) H₂ + definition eq.rec_symm {A : Type} {a₀ : A} {P : Π⦃a₁⦄, a₁ = a₀ → Type} + (H : P idp) ⦃a₁ : A⦄ (p : a₁ = a₀) : P p := + begin + cases p, exact H + end + /- Theorems for moving things around in equations -/ definition con_eq_of_eq_inv_con {p : x = z} {q : y = z} {r : y = x} : @@ -234,6 +240,9 @@ namespace eq protected definition homotopy.refl [refl] [reducible] [unfold_full] (f : Πx, P x) : f ~ f := λ x, idp + protected definition homotopy.rfl [reducible] [unfold_full] {f : Πx, P x} : f ~ f := + homotopy.refl f + protected definition homotopy.symm [symm] [reducible] [unfold_full] {f g : Πx, P x} (H : f ~ g) : g ~ f := λ x, (H x)⁻¹ @@ -242,6 +251,9 @@ namespace eq (H1 : f ~ g) (H2 : g ~ h) : f ~ h := λ x, H1 x ⬝ H2 x + infix ` ⬝hty `:75 := homotopy.trans + postfix `⁻¹ʰᵗʸ`:(max+1) := homotopy.symm + definition hwhisker_left [unfold_full] (g : B → C) {f f' : A → B} (H : f ~ f') : g ∘ f ~ g ∘ f' := λa, ap g (H a) @@ -250,6 +262,19 @@ namespace eq g ∘ f ~ g' ∘ f := λa, H (f a) + definition compose_id (f : A → B) : f ∘ id ~ f := + by reflexivity + + definition id_compose (f : A → B) : id ∘ f ~ f := + by reflexivity + + definition compose2 {A B C : Type} {g g' : B → C} {f f' : A → B} + (p : g ~ g') (q : f ~ f') : g ∘ f ~ g' ∘ f' := + hwhisker_right f p ⬝hty hwhisker_left g' q + + definition hassoc {A B C D : Type} (h : C → D) (g : B → C) (f : A → B) : (h ∘ g) ∘ f ~ h ∘ (g ∘ f) := + λa, idp + definition homotopy_of_eq {f g : Πx, P x} (H1 : f = g) : f ~ g := H1 ▸ homotopy.refl f @@ -277,14 +302,6 @@ namespace eq definition ap011 [unfold 9] (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := by cases Ha; exact ap (f a) Hb - definition ap_eq_ap011_left (f : A → B → C) (Ha : a = a') (b : B) : - ap (λa, f a b) Ha = ap011 f Ha idp := - by induction Ha; reflexivity - - definition ap_eq_ap011_right (f : A → B → C) (a : A) (Hb : b = b') : - ap (f a) Hb = ap011 f idp Hb := - by reflexivity - /- More theorems for moving things around in equations -/ definition tr_eq_of_eq_inv_tr {P : A → Type} {x y : A} {p : x = y} {u : P x} {v : P y} : @@ -453,6 +470,22 @@ namespace eq ap h (ap10 p a) = ap10 (ap (λ f', h ∘ f') p) a:= by induction p; reflexivity + /- some lemma's about ap011 -/ + + definition ap_eq_ap011_left (f : A → B → C) (Ha : a = a') (b : B) : + ap (λa, f a b) Ha = ap011 f Ha idp := + by induction Ha; reflexivity + + definition ap_eq_ap011_right (f : A → B → C) (a : A) (Hb : b = b') : + ap (f a) Hb = ap011 f idp Hb := + by reflexivity + + definition ap_ap011 {A B C D : Type} (g : C → D) (f : A → B → C) {a a' : A} {b b' : B} + (p : a = a') (q : b = b') : ap g (ap011 f p q) = ap011 (λa b, g (f a b)) p q := + begin + induction p, exact (ap_compose g (f a) q)⁻¹ + end + /- Transport and the groupoid structure of paths -/ diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 95c1a22c0..96f318dcb 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -281,6 +281,11 @@ namespace eq (q : b =[p] b₂) : f b =[p] g b₂ := by induction q; exact apo10 r b + definition apo011 {A : Type} {B C D : A → Type} {a a' : A} {p : a = a'} {b : B a} {b' : B a'} + {c : C a} {c' : C a'} (f : Π⦃a⦄, B a → C a → D a) (q : b =[p] b') (r : c =[p] c') : + f b c =[p] f b' c' := + begin induction q, induction r using idp_rec_on, exact idpo end + definition apdo011 {A : Type} {B : A → Type} {C : Π⦃a⦄, B a → Type} (f : Π⦃a⦄ (b : B a), C b) {a a' : A} (p : a = a') {b : B a} {b' : B a'} (q : b =[p] b') : f b =[apd011 C p q] f b' := @@ -445,5 +450,4 @@ namespace eq apd0111 f (ap k p) (pathover_ap B k (apo l q)) (pathover_tro _ (m c)) := by induction q; reflexivity - end eq diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index a86e4bdc7..bf504c0bb 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -145,6 +145,8 @@ namespace is_trunc definition center (A : Type) [H : is_contr A] : A := contr_internal.center (is_trunc.to_internal -2 A) + definition center' {A : Type} (H : is_contr A) : A := center A + definition center_eq [H : is_contr A] (a : A) : !center = a := contr_internal.center_eq (is_trunc.to_internal -2 A) a @@ -337,13 +339,17 @@ namespace is_trunc {a a₂ : A} (p : a = a₂) (c : C a) (c₂ : C a₂) - definition is_prop.elimo [H : is_prop (C a)] : c =[p] c₂ := - pathover_of_eq_tr !is_prop.elim - definition is_trunc_pathover [instance] (n : ℕ₋₂) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) := is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr + definition is_prop.elimo [H : is_prop (C a)] : c =[p] c₂ := + pathover_of_eq_tr !is_prop.elim + + definition is_prop_elimo_self {A : Type} (B : A → Type) {a : A} (b : B a) {H : is_prop (B a)} : + @is_prop.elimo A B a a idp b b H = idpo := + !is_prop.elim + variables {p c c₂} theorem is_set.elimo (q q' : c =[p] c₂) [H : is_set (C a)] : q = q' := !is_prop.elim diff --git a/hott/prop_trunc.hlean b/hott/prop_trunc.hlean index 52b44412b..e242e43ce 100644 --- a/hott/prop_trunc.hlean +++ b/hott/prop_trunc.hlean @@ -35,7 +35,7 @@ namespace is_trunc induction (P a b), apply idp}, end - definition is_prop_is_trunc [instance] (n : trunc_index) : + definition is_prop_is_trunc (n : trunc_index) : Π (A : Type), is_prop (is_trunc n A) := begin induction n, @@ -50,4 +50,10 @@ namespace is_trunc apply equiv.to_is_equiv, apply is_trunc.pi_char}, end + + local attribute is_prop_is_trunc [instance] + definition is_trunc_succ_is_trunc [instance] (n m : ℕ₋₂) (A : Type) : + is_trunc (n.+1) (is_trunc m A) := + !is_trunc_succ_of_is_prop + end is_trunc diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 37f89ecba..3c450bf08 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -146,26 +146,7 @@ namespace fiber : ppoint f ~* pmap.mk pr1 idp ∘* pfiber.sigma_char f := !phomotopy.refl - definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := - pequiv_of_equiv - (calc pfiber (Ω→ f) ≃ Σ(p : Point A = Point A), ap1 f p = rfl - : (fiber.sigma_char (ap1 f) (Point (Ω B))) - ... ≃ Σ(p : Point A = Point A), (respect_pt f) = ap f p ⬝ (respect_pt f) - : (sigma_equiv_sigma_right (λp, - calc (ap1 f p = rfl) ≃ !respect_pt⁻¹ ⬝ (ap f p ⬝ !respect_pt) = rfl - : equiv_eq_closed_left _ (con.assoc _ _ _) - ... ≃ ap f p ⬝ (respect_pt f) = (respect_pt f) - : eq_equiv_inv_con_eq_idp - ... ≃ (respect_pt f) = ap f p ⬝ (respect_pt f) - : eq_equiv_eq_symm)) - ... ≃ fiber.mk (Point A) (respect_pt f) = fiber.mk pt (respect_pt f) - : fiber_eq_equiv - ... ≃ Ω (pfiber f) - : erfl) - (begin cases f with f p, cases A with A a, cases B with B b, esimp at p, esimp at f, - induction p, reflexivity end) - - definition pfiber_equiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) + definition pfiber_pequiv_of_phomotopy {A B : Type*} {f g : A →* B} (h : f ~* g) : pfiber f ≃* pfiber g := begin fapply pequiv_of_equiv, @@ -202,12 +183,125 @@ namespace fiber { apply eq_pathover_Fl' } end - definition pfiber_equiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) + definition pfiber_pequiv_of_square {A B C D : Type*} {f : A →* B} {g : C →* D} (h : A ≃* C) (k : B ≃* D) (s : k ∘* f ~* g ∘* h) : pfiber f ≃* pfiber g := calc pfiber f ≃* pfiber (k ∘* f) : pequiv_postcompose - ... ≃* pfiber (g ∘* h) : pfiber_equiv_of_phomotopy s + ... ≃* pfiber (g ∘* h) : pfiber_pequiv_of_phomotopy s ... ≃* pfiber g : pequiv_precompose + definition pcompose_ppoint {A B : Type*} (f : A →* B) : f ∘* ppoint f ~* pconst (pfiber f) B := + begin + fapply phomotopy.mk, + { exact point_eq }, + { exact !idp_con⁻¹ } + end + + definition point_fiber_eq {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + (p : point x = point y) (q : point_eq x = ap f p ⬝ point_eq y) : + ap point (fiber_eq p q) = p := + begin + induction x with a r, induction y with a' s, esimp at *, induction p, + induction q using eq.rec_symm, induction s, reflexivity + end + + definition fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} (x y : fiber f b) : + 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 + ... ≃ Σ(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, + calc point_eq x =[p] point_eq y ≃ point_eq x = ap f p ⬝ point_eq y : eq_pathover_equiv_Fl + ... ≃ ap f p ⬝ point_eq y = point_eq x : eq_equiv_eq_symm + ... ≃ (point_eq x)⁻¹ ⬝ (ap f p ⬝ point_eq y) = idp : eq_equiv_inv_con_eq_idp + ... ≃ (point_eq x)⁻¹ ⬝ ap f p ⬝ point_eq y = idp : equiv_eq_closed_left _ !con.assoc⁻¹) + ... ≃ fiber (ap1_gen f (point_eq x) (point_eq y)) (idpath b) : fiber.sigma_char + + definition loop_pfiber [constructor] {A B : Type*} (f : A →* B) : Ω (pfiber f) ≃* pfiber (Ω→ f) := + pequiv_of_equiv (fiber_eq_equiv_fiber pt pt) + begin + induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity + end + + definition pfiber_loop_space {A B : Type*} (f : A →* B) : pfiber (Ω→ f) ≃* Ω (pfiber f) := + (loop_pfiber f)⁻¹ᵉ* + + definition point_fiber_eq_equiv_fiber {A B : Type} {f : A → B} {b : B} {x y : fiber f b} + (p : x = y) : point (fiber_eq_equiv_fiber x y p) = ap1_gen point idp idp p := + by induction p; reflexivity + + lemma ppoint_loop_pfiber {A B : Type*} (f : A →* B) : + ppoint (Ω→ f) ∘* loop_pfiber f ~* Ω→ (ppoint f) := + phomotopy.mk (point_fiber_eq_equiv_fiber) + begin + induction f with f f₀, induction B with B b₀, esimp at (f,f₀), induction f₀, reflexivity + end + + lemma ppoint_loop_pfiber_inv {A B : Type*} (f : A →* B) : + Ω→ (ppoint f) ∘* (loop_pfiber f)⁻¹ᵉ* ~* ppoint (Ω→ f) := + (phomotopy_pinv_right_of_phomotopy (ppoint_loop_pfiber f))⁻¹* + + lemma pfiber_pequiv_of_phomotopy_ppoint {A B : Type*} {f g : A →* B} (h : f ~* g) + : ppoint g ∘* pfiber_pequiv_of_phomotopy h ~* ppoint f := + begin + induction f with f f₀, induction g with g g₀, induction h with h h₀, induction B with B b₀, + esimp at *, induction h₀, induction g₀, + fapply phomotopy.mk, + { reflexivity }, + { esimp [pfiber_pequiv_of_phomotopy], exact !point_fiber_eq⁻¹ } + end + + lemma pequiv_postcompose_ppoint {A B B' : Type*} (f : A →* B) (g : B ≃* B') + : ppoint f ∘* fiber.pequiv_postcompose f g ~* ppoint (g ∘* f) := + begin + induction f with f f₀, induction g with g hg g₀, induction B with B b₀, + induction B' with B' b₀', esimp at *, induction g₀, induction f₀, + fapply phomotopy.mk, + { reflexivity }, + { esimp [pequiv_postcompose], symmetry, + refine !ap_compose⁻¹ ⬝ _, apply ap_constant } + end + + lemma pequiv_precompose_ppoint {A A' B : Type*} (f : A →* B) (g : A' ≃* A) + : ppoint f ∘* fiber.pequiv_precompose f g ~* g ∘* ppoint (f ∘* g) := + begin + induction f with f f₀, induction g with g hg g₀, induction B with B b₀, + induction A with A a₀', esimp at *, induction g₀, induction f₀, + reflexivity, + end + + definition pfiber_pequiv_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_pequiv_of_square h k s ~* h ∘* ppoint f := + begin + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !pequiv_precompose_ppoint ⬝* _, + refine !passoc ⬝* _, + apply pwhisker_left, + refine !passoc⁻¹* ⬝* _, + refine pwhisker_right _ !pfiber_pequiv_of_phomotopy_ppoint ⬝* _, + apply pinv_right_phomotopy_of_phomotopy, + refine !pequiv_postcompose_ppoint⁻¹*, + end + + -- this breaks certain proofs if it is an instance + definition is_trunc_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) + [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (fiber f b) := + is_trunc_equiv_closed_rev n !fiber.sigma_char + + definition is_trunc_pfiber (n : ℕ₋₂) {A B : Type*} (f : A →* B) + [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) := + is_trunc_fiber n f pt + + definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) [is_contr B] : + fiber f b ≃ A := + !fiber.sigma_char ⬝e !sigma_equiv_of_is_contr_right + + definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] : + pfiber f ≃* A := + pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp + end fiber open function is_equiv diff --git a/hott/types/int/hott.hlean b/hott/types/int/hott.hlean index 9e9df1c02..3a965c8c1 100644 --- a/hott/types/int/hott.hlean +++ b/hott/types/int/hott.hlean @@ -6,7 +6,7 @@ Author: Floris van Doorn Theorems about the integers specific to HoTT -/ -import .basic types.eq arity algebra.bundled +import .order types.eq arity algebra.bundled open core eq is_equiv equiv algebra is_trunc open nat (hiding pred) @@ -28,6 +28,12 @@ namespace int AddAbGroup.mk ℤ _ notation `agℤ` := AbGroup_int + + definition ring_int : Ring := + Ring.mk ℤ _ + + notation `rℤ` := ring_int + end definition is_equiv_succ [constructor] [instance] : is_equiv succ := @@ -43,6 +49,17 @@ namespace int (λb g, f ⬝e g) (λb g, g ⬝e f⁻¹ᵉ) + definition max0 : ℤ → ℕ + | (of_nat n) := n + | (-[1+ n]) := 0 + + lemma le_max0 : Π(n : ℤ), n ≤ of_nat (max0 n) + | (of_nat n) := proof le.refl n qed + | (-[1+ n]) := proof unit.star qed + + lemma le_of_max0_le {n : ℤ} {m : ℕ} (h : max0 n ≤ m) : n ≤ of_nat m := + le.trans (le_max0 n) (of_nat_le_of_nat_of_le h) + -- definition iterate_trans {A : Type} (f : A ≃ A) (a : ℤ) -- : iterate f a ⬝e f = iterate f (a + 1) := -- sorry diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index f4bcf4460..874883dbc 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -6,9 +6,9 @@ Author: Floris van Doorn Theorems about the natural numbers specific to HoTT -/ -import .order types.pointed +import .order types.pointed .sub -open is_trunc unit empty eq equiv algebra pointed +open is_trunc unit empty eq equiv algebra pointed is_equiv equiv function namespace nat definition is_prop_le [instance] (n m : ℕ) : is_prop (n ≤ m) := @@ -194,5 +194,44 @@ namespace nat definition is_at_least_two_bit1 [constructor] (n : ℕ) [H : is_succ n] : is_at_least_two (bit1 n) := by exact _ + /- some facts about iterate -/ + + definition iterate_succ {A : Type} (f : A → A) (n : ℕ) (x : A) : + f^[succ n] x = f^[n] (f x) := + by induction n with n p; reflexivity; exact ap f p + + lemma iterate_sub {A : Type} (f : A ≃ A) {n m : ℕ} (h : n ≥ m) (a : A) : + iterate f (n - m) a = iterate f n (iterate f⁻¹ m a) := + begin + revert n h, induction m with m p: intro n h, + { reflexivity }, + { cases n with n, exfalso, apply not_succ_le_zero _ h, + rewrite [succ_sub_succ], refine p n (le_of_succ_le_succ h) ⬝ _, + refine ap (f^[n]) _ ⬝ !iterate_succ⁻¹, exact !to_right_inv⁻¹ } + end + + definition iterate_commute {A : Type} {f g : A → A} (n : ℕ) (h : f ∘ g ~ g ∘ f) : + iterate f n ∘ g ~ g ∘ iterate f n := + by induction n with n IH; reflexivity; exact λx, ap f (IH x) ⬝ !h + + definition iterate_equiv {A : Type} (f : A ≃ A) (n : ℕ) : A ≃ A := + equiv.mk (iterate f n) + (by induction n with n IH; apply is_equiv_id; exact is_equiv_compose f (iterate f n)) + + definition iterate_inv {A : Type} (f : A ≃ A) (n : ℕ) : + (iterate_equiv f n)⁻¹ ~ iterate f⁻¹ n := + begin + induction n with n p: intro a, + reflexivity, + exact p (f⁻¹ a) ⬝ !iterate_succ⁻¹ + end + + definition iterate_left_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f⁻¹ᵉ^[n] (f^[n] a) = a := + (iterate_inv f n (f^[n] a))⁻¹ ⬝ to_left_inv (iterate_equiv f n) a + + definition iterate_right_inv {A : Type} (f : A ≃ A) (n : ℕ) (a : A) : f^[n] (f⁻¹ᵉ^[n] a) = a := + ap (f^[n]) (iterate_inv f n a)⁻¹ ⬝ to_right_inv (iterate_equiv f n) a + + end nat diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 74b19ef7c..cdf1aa77d 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -326,6 +326,11 @@ namespace pi local attribute ne [reducible] theorem is_prop_ne [instance] {A : Type} (a b : A) : is_prop (a ≠ b) := _ + definition is_contr_pi_of_neg {A : Type} (B : A → Type) (H : ¬ A) : is_contr (Πa, B a) := + begin + apply is_contr.mk (λa, empty.elim (H a)), intro f, apply eq_of_homotopy, intro x, contradiction + end + /- Symmetry of Π -/ definition is_equiv_flip [instance] {P : A → A' → Type} : is_equiv (@function.flip A A' P) := diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 9a6d88164..61dfee981 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -3,8 +3,10 @@ Copyright (c) 2014-2016 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jakob von Raumer, Floris van Doorn -Ported from Coq HoTT +Early library ported from Coq HoTT, but greatly extended since. The basic definitions are in init.pointed + +See also .pointed2 -/ import .nat.basic ..arity ..prop_trunc @@ -126,6 +128,10 @@ namespace pointed infixr ` ∘* `:60 := pcompose + definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) + : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := + idp + definition passoc [constructor] (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) := phomotopy.mk (λa, idp) abstract !idp_con ⬝ whisker_right _ (!ap_con ⬝ whisker_right _ !ap_compose'⁻¹) ⬝ !con.assoc end @@ -348,6 +354,10 @@ namespace pointed definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g := phomotopy.mk (ap010 pmap.to_fun p) begin induction p, apply idp_con end + definition phomotopy_of_eq_idp {A B : Type*} (f : A →* B) : + phomotopy_of_eq idp = phomotopy.refl f := + idp + definition pconcat_eq [constructor] {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g = h) : f ~* h := p ⬝* phomotopy_of_eq q @@ -359,6 +369,10 @@ namespace pointed infix ` ⬝*p `:75 := pconcat_eq infix ` ⬝p* `:75 := eq_pconcat + definition pr1_phomotopy_eq {A B : Type*} {f g : A →* B} {p q : f ~* g} (r : p = q) (a : A) : + p a = q a := + ap010 to_homotopy r a + definition pmap_eq_equiv_internal {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) := calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g : eq_equiv_fn_eq pmap.sigma_char f g @@ -397,6 +411,19 @@ namespace pointed definition eq_of_phomotopy (p : f ~* g) : f = g := to_inv (pmap_eq_equiv f g) p + definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : + eq_of_phomotopy (phomotopy.refl f) = idpath f := + begin + apply to_inv_eq_of_eq, reflexivity + end + + definition phomotopy_of_homotopy {X Y : Type*} {f g : X →* Y} (h : f ~ g) [is_set Y] : f ~* g := + begin + fapply phomotopy.mk, + { exact h }, + { apply is_set.elim } + end + -- TODO: flip arguments in s definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g := eq_of_phomotopy (phomotopy.mk r s⁻¹) @@ -404,6 +431,37 @@ namespace pointed definition pmap_eq_of_homotopy {A B : Type*} {f g : A →* B} [is_set B] (p : f ~ g) : f = g := pmap_eq p !is_set.elim + definition phomotopy_of_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : + phomotopy_of_eq (eq_of_phomotopy p) = p := + to_right_inv (pmap_eq_equiv f g) p + + definition phomotopy_rec_on_eq [recursor] {A B : Type*} {f g : A →* B} + {Q : (f ~* g) → Type} (p : f ~* g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : Q p := + phomotopy_of_eq_of_phomotopy p ▸ H (eq_of_phomotopy p) + + definition phomotopy_rec_on_idp [recursor] {A B : Type*} {f : A →* B} + {Q : Π{g}, (f ~* g) → Type} {g : A →* B} (p : f ~* g) (H : Q (phomotopy.refl f)) : Q p := + begin + induction p using phomotopy_rec_on_eq, + induction q, exact H + end + + definition phomotopy_rec_on_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} + {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : + phomotopy_rec_on_eq (phomotopy_of_eq p) H = H p := + begin + unfold phomotopy_rec_on_eq, + refine ap (λp, p ▸ _) !adj ⬝ _, + refine !tr_compose⁻¹ ⬝ _, + apply apdt + end + + definition phomotopy_rec_on_idp_refl {A B : Type*} (f : A →* B) + {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : + phomotopy_rec_on_idp phomotopy.rfl H = H := + !phomotopy_rec_on_eq_phomotopy_of_eq + + /- adjunction between (-)₊ : Type → Type* and pType.carrier : Type* → Type -/ definition pmap_equiv_left (A : Type) (B : Type*) : A₊ →* B ≃ (A → B) := begin fapply equiv.MK, @@ -440,12 +498,21 @@ namespace pointed resulting pointed homotopy is reflexivity -/ definition pap (F : (A →* B) → (C →* D)) {f g : A →* B} (p : f ~* g) : F f ~* F g := - phomotopy.mk (ap010 (λf, pmap.to_fun (F f)) (eq_of_phomotopy p)) - begin cases eq_of_phomotopy p, apply idp_con end + begin + induction p using phomotopy_rec_on_idp, reflexivity + end + + definition pap_refl (F : (A →* B) → (C →* D)) (f : A →* B) : + pap F (phomotopy.refl f) = phomotopy.refl (F f) := + !phomotopy_rec_on_idp_refl definition ap1_phomotopy {f g : A →* B} (p : f ~* g) : Ω→ f ~* Ω→ g := pap Ω→ p + definition ap1_phomotopy_refl {X Y : Type*} (f : X →* Y) : + ap1_phomotopy (phomotopy.refl f) = phomotopy.refl (Ω→ f) := + !pap_refl + --a proof not using function extensionality: definition ap1_phomotopy_explicit {f g : A →* B} (p : f ~* g) : Ω→ f ~* Ω→ g := begin @@ -465,6 +532,26 @@ namespace pointed { exact ap1_phomotopy IH} end + -- the following two definitiongs are mostly the same, maybe we should remove one + definition ap_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : + ap (λf : A →* B, f a) (eq_of_phomotopy p) = p a := + ap010 to_homotopy (phomotopy_of_eq_of_phomotopy p) a + + definition to_fun_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) (a : A) : + ap010 pmap.to_fun (eq_of_phomotopy p) a = p a := + begin + induction p using phomotopy_rec_on_idp, + exact ap (λx, ap010 pmap.to_fun x a) !eq_of_phomotopy_refl + end + + definition ap1_eq_of_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) : + ap Ω→ (eq_of_phomotopy p) = eq_of_phomotopy (ap1_phomotopy p) := + begin + induction p using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !ap1_phomotopy_refl⁻¹ + end + /- pointed homotopies between the given pointed maps -/ definition ap1_pid [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) := @@ -509,6 +596,20 @@ namespace pointed definition ap1_pconst [constructor] (A B : Type*) : Ω→(pconst A B) ~* pconst (Ω A) (Ω B) := phomotopy.mk (λp, ap1_gen_idp_left (const A pt) p ⬝ ap_constant p pt) rfl + definition ap1_gen_con_left {A B : Type} {a a' : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ q₁ : b₀ = b₁} {q₀' q₁' : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f a' = q₁) (r₀' : f' a = q₀') (r₁' : f' a' = q₁') (p : a = a') : + ap1_gen (λa, f a ⬝ f' a) (r₀ ◾ r₀') (r₁ ◾ r₁') p = + whisker_right q₀' (ap1_gen f r₀ r₁ p) ⬝ whisker_left q₁ (ap1_gen f' r₀' r₁' p) := + begin induction r₀, induction r₁, induction r₀', induction r₁', induction p, reflexivity end + + definition ap1_gen_con_left_idp {A B : Type} {a : A} {b₀ b₁ b₂ : B} + {f : A → b₀ = b₁} {f' : A → b₁ = b₂} {q₀ : b₀ = b₁} {q₁ : b₁ = b₂} + (r₀ : f a = q₀) (r₁ : f' a = q₁) : + ap1_gen_con_left r₀ r₀ r₁ r₁ idp = + !con.left_inv ⬝ (ap (whisker_right q₁) !con.left_inv ◾ ap (whisker_left _) !con.left_inv)⁻¹ := + begin induction r₀, induction r₁, reflexivity end + definition ptransport_change_eq [constructor] {A : Type} (B : A → Type*) {a a' : A} {p q : a = a'} (r : p = q) : ptransport B p ~* ptransport B q := phomotopy.mk (λb, ap (λp, transport B p b) r) begin induction r, apply idp_con end @@ -655,6 +756,9 @@ namespace pointed : pequiv.to_pmap (f ⬝e* g) = g ∘* f := !to_pmap_pequiv_of_pmap + definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := + λx, idp + definition pequiv_change_fun [constructor] (f : A ≃* B) (f' : A →* B) (Heq : f ~ f') : A ≃* B := pequiv_of_pmap f' (is_equiv.homotopy_closed f Heq) @@ -892,6 +996,10 @@ namespace pointed definition loop_pequiv_loop [constructor] (f : A ≃* B) : Ω A ≃* Ω B := loopn_pequiv_loopn 1 f + 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) + definition to_pmap_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : loopn_pequiv_loopn n f ~* apn n f := !to_pmap_pequiv_MK2 @@ -919,6 +1027,12 @@ namespace pointed loop_pequiv_loop (pequiv.refl A) ~* pequiv.refl (Ω A) := loopn_pequiv_loopn_rfl 1 A + definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : + Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* := + begin + refine !to_pinv_pequiv_MK2⁻¹* + end + definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') : ppmap A B →* ppmap A' B' := pmap.mk (λh, g ∘* h ∘* f) @@ -950,20 +1064,6 @@ namespace pointed exact !con.right_inv⁻¹ ⬝ ((!idp_con⁻¹ ⬝ !ap_id⁻¹) ◾ (!ap_id⁻¹⁻² ⬝ !idp_con⁻¹)), } end -/- -- TODO - definition pmap_pequiv_pmap {A A' B B' : Type*} (f : A ≃* A') (g : B ≃* B') : - ppmap A B ≃* ppmap A' B' := - pequiv.MK (pmap_functor f⁻¹ᵉ* g) (pmap_functor f g⁻¹ᵉ*) - abstract begin - intro a, esimp, apply pmap_eq, - { esimp, }, - { } - end end - abstract begin - - end end --/ - /- properties of iterated loop space -/ variable (A) definition loopn_succ_in (n : ℕ) : Ω[succ n] A ≃* Ω[n] (Ω A) := @@ -1071,7 +1171,7 @@ namespace pointed refine pwhisker_left g !pleft_inv ⬝* !pcompose_pid, }, end - definition loop_pmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := + definition loop_ppmap_commute (A B : Type*) : Ω(ppmap A B) ≃* (ppmap A (Ω B)) := pequiv_of_equiv (calc Ω(ppmap A B) ≃ (pconst A B ~* pconst A B) : pmap_eq_equiv _ _ ... ≃ Σ(p : pconst A B ~ pconst A B), p pt ⬝ rfl = rfl : phomotopy.sigma_char @@ -1084,7 +1184,7 @@ namespace pointed definition papply_pcompose [constructor] {A : Type*} (B : Type*) (a : A) : ppmap A B →* B := pmap.mk (λ(f : A →* B), f a) idp - definition pmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := + definition ppmap_pbool_pequiv [constructor] (B : Type*) : ppmap pbool B ≃* B := begin fapply pequiv.MK, { exact papply B tt }, diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean new file mode 100644 index 000000000..80d04c164 --- /dev/null +++ b/hott/types/pointed2.hlean @@ -0,0 +1,847 @@ +/- +Copyright (c) 2017 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +More results about pointed types. + +Contains +- squares of pointed maps, +- equalities between pointed homotopies and +- squares between pointed homotopies +- pointed maps into and out of (ppmap A B), the pointed type of pointed maps from A to B +-/ + + +import algebra.homotopy_group eq2 + +open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function + +namespace pointed + + + section psquare + /- + Squares of pointed maps + + We treat expressions of the form + psquare f g h k :≡ k ∘* f ~* g ∘* h + as squares, where f is the top, g is the bottom, h is the left face and k is the right face. + Then the following are operations on squares + -/ + + variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} + {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} + {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} + {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} + {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} + + definition psquare [reducible] (f₁₀ : A₀₀ →* A₂₀) (f₁₂ : A₀₂ →* A₂₂) + (f₀₁ : A₀₀ →* A₀₂) (f₂₁ : A₂₀ →* A₂₂) : Type := + f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ + + definition psquare_of_phomotopy (p : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁) : psquare f₁₀ f₁₂ f₀₁ f₂₁ := + p + + definition phomotopy_of_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : f₂₁ ∘* f₁₀ ~* f₁₂ ∘* f₀₁ := + p + + definition phdeg_square {f f' : A →* A'} (p : f ~* f') : psquare !pid !pid f f' := + !pcompose_pid ⬝* p⁻¹* ⬝* !pid_pcompose⁻¹* + definition pvdeg_square {f f' : A →* A'} (p : f ~* f') : psquare f f' !pid !pid := + !pid_pcompose ⬝* p ⬝* !pcompose_pid⁻¹* + + variables (f₀₁ f₁₀) + definition phrefl : psquare !pid !pid f₀₁ f₀₁ := phdeg_square phomotopy.rfl + definition pvrefl : psquare f₁₀ f₁₀ !pid !pid := pvdeg_square phomotopy.rfl + variables {f₀₁ f₁₀} + definition phrfl : psquare !pid !pid f₀₁ f₀₁ := phrefl f₀₁ + definition pvrfl : psquare f₁₀ f₁₀ !pid !pid := pvrefl f₁₀ + + definition phconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₃₀ f₃₂ f₂₁ f₄₁) : + psquare (f₃₀ ∘* f₁₀) (f₃₂ ∘* f₁₂) f₀₁ f₄₁ := + !passoc⁻¹* ⬝* pwhisker_right f₁₀ q ⬝* !passoc ⬝* pwhisker_left f₃₂ p ⬝* !passoc⁻¹* + + definition pvconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + psquare f₁₀ f₁₄ (f₀₃ ∘* f₀₁) (f₂₃ ∘* f₂₁) := + !passoc ⬝* pwhisker_left _ p ⬝* !passoc⁻¹* ⬝* pwhisker_right _ q ⬝* !passoc + + definition phinverse {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀⁻¹ᵉ* f₁₂⁻¹ᵉ* f₂₁ f₀₁ := + !pid_pcompose⁻¹* ⬝* pwhisker_right _ (pleft_inv f₁₂)⁻¹* ⬝* !passoc ⬝* + pwhisker_left _ + (!passoc⁻¹* ⬝* pwhisker_right _ p⁻¹* ⬝* !passoc ⬝* pwhisker_left _ !pright_inv ⬝* !pcompose_pid) + + definition pvinverse {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₂ f₁₀ f₀₁⁻¹ᵉ* f₂₁⁻¹ᵉ* := + (phinverse p⁻¹*)⁻¹* + + definition phomotopy_hconcat (q : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀ f₁₂ f₀₁' f₂₁ := + p ⬝* pwhisker_left f₁₂ q⁻¹* + + definition hconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₂₁' ~* f₂₁) : + psquare f₁₀ f₁₂ f₀₁ f₂₁' := + pwhisker_right f₁₀ q ⬝* p + + definition phomotopy_vconcat (q : f₁₀' ~* f₁₀) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare f₁₀' f₁₂ f₀₁ f₂₁ := + pwhisker_left f₂₁ q ⬝* p + + definition vconcat_phomotopy (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : f₁₂' ~* f₁₂) : + psquare f₁₀ f₁₂' f₀₁ f₂₁ := + p ⬝* pwhisker_right f₀₁ q⁻¹* + + infix ` ⬝h* `:73 := phconcat + infix ` ⬝v* `:73 := pvconcat + infixl ` ⬝hp* `:72 := hconcat_phomotopy + infixr ` ⬝ph* `:72 := phomotopy_hconcat + infixl ` ⬝vp* `:72 := vconcat_phomotopy + infixr ` ⬝pv* `:72 := phomotopy_vconcat + postfix `⁻¹ʰ*`:(max+1) := phinverse + postfix `⁻¹ᵛ*`:(max+1) := pvinverse + + definition pwhisker_tl (f : A →* A₀₀) (q : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (f₁₀ ∘* f) f₁₂ (f₀₁ ∘* f) f₂₁ := + !passoc⁻¹* ⬝* pwhisker_right f q ⬝* !passoc + + definition ap1_psquare (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→ f₁₀) (Ω→ f₁₂) (Ω→ f₀₁) (Ω→ f₂₁) := + !ap1_pcompose⁻¹* ⬝* ap1_phomotopy p ⬝* !ap1_pcompose + + definition apn_psquare (n : ℕ) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (Ω→[n] f₁₀) (Ω→[n] f₁₂) (Ω→[n] f₀₁) (Ω→[n] f₂₁) := + !apn_pcompose⁻¹* ⬝* apn_phomotopy n p ⬝* !apn_pcompose + + definition ptrunc_functor_psquare (n : ℕ₋₂) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (ptrunc_functor n f₁₀) (ptrunc_functor n f₁₂) + (ptrunc_functor n f₀₁) (ptrunc_functor n f₂₁) := + !ptrunc_functor_pcompose⁻¹* ⬝* ptrunc_functor_phomotopy n p ⬝* !ptrunc_functor_pcompose + + 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 + + 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₂₁) := + begin + induction H with n, exact to_homotopy (ptrunc_functor_psquare 0 (apn_psquare (succ n) p)) + end + + end psquare + + definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : + f ~* pconst punit A := + begin + fapply phomotopy.mk, + { intro u, induction u, exact respect_pt f }, + { reflexivity } + end + + definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) := + is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*) + + 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 := + calc + h = k ≃ phomotopy.sigma_char _ _ h = phomotopy.sigma_char _ _ k + : eq_equiv_fn_eq (phomotopy.sigma_char f g) h k + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + pathover (λp, p pt ⬝ respect_pt g = respect_pt f) (to_homotopy_pt h) p (to_homotopy_pt k) + : sigma_eq_equiv _ _ + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + to_homotopy_pt h = ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k + : sigma_equiv_sigma_right (λp, eq_pathover_equiv_Fl p (to_homotopy_pt h) (to_homotopy_pt k)) + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + ap (λq, q pt ⬝ respect_pt g) p ⬝ to_homotopy_pt k = to_homotopy_pt h + : sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _) + ... ≃ Σ(p : to_homotopy h = to_homotopy k), + whisker_right (respect_pt g) (apd10 p pt) ⬝ to_homotopy_pt k = to_homotopy_pt h + : 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 + + 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 := + to_inv (phomotopy_eq_equiv h k) ⟨p, q⟩ + + definition phomotopy_eq' {A B : Type*} {f g : A →* B} {h k : f ~* g} (p : to_homotopy h ~ to_homotopy k) + (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := + phomotopy_eq p (eq_of_square q)⁻¹ + + definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := + begin + induction A with A a₀, induction B with B b₀, + induction f with f f₀, induction g with g g₀, induction p with p p₀, + esimp at *, induction g₀, induction p₀, + reflexivity + end + + definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) : + eq_of_phomotopy (p ⬝* q) = eq_of_phomotopy p ⬝ eq_of_phomotopy q := + begin + induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, + exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹ + end + + definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := + begin + induction p using phomotopy_rec_on_idp, + induction A with A a₀, induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) + (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := + begin + induction r using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + induction p using phomotopy_rec_on_idp, + induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := + begin + induction B with B b₀, + induction f with f f₀, esimp at *, induction f₀, + reflexivity + end + + definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := + phomotopy_eq (λa, !inv_inv) + begin + induction p using phomotopy_rec_on_idp, induction f with f f₀, induction B with B b₀, + esimp at *, induction f₀, reflexivity + end + + definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !refl_trans ⬝ !refl_symm + end + + definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := + begin + induction p using phomotopy_rec_on_idp, exact !trans_refl ⬝ !refl_symm + end + + definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} + (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := + ap011 phomotopy.trans r s + + definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} + {p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' := + ap011 pcompose2 r s + + definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* := + ap phomotopy.symm r + + infixl ` ◾** `:80 := pointed.trans2 + infixl ` ◽* `:81 := pointed.pcompose3 + postfix `⁻²**`:(max+1) := pointed.symm2 + + definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) : + (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* := + begin + induction p using phomotopy_rec_on_idp, induction q using phomotopy_rec_on_idp, + exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹ + end + + definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} + (s : q = q') : p ⬝* q = p ⬝* q' := + idp ◾** s + + definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) + (r : p = p') : p ⬝* q = p' ⬝* q := + r ◾** idp + + definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : + pwhisker_left g (phomotopy.refl f) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pwhisker_right_refl {A B C : Type*} (f : A →* B) (g : B →* C) : + pwhisker_right f (phomotopy.refl g) = phomotopy.refl (g ∘* f) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, + induction f with f f₀, induction g with g g₀, + esimp at *, induction g₀, induction f₀, reflexivity + end + + definition pcompose2_refl {A B C : Type*} (g : B →* C) (f : A →* B) : + phomotopy.refl g ◾* phomotopy.refl f = phomotopy.rfl := + !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ !refl_trans + + definition pcompose2_refl_left {A B C : Type*} (g : B →* C) {f f' : A →* B} (p : f ~* f') : + phomotopy.rfl ◾* p = pwhisker_left g p := + !pwhisker_right_refl ◾** idp ⬝ !refl_trans + + definition pcompose2_refl_right {A B C : Type*} {g g' : B →* C} (f : A →* B) (p : g ~* g') : + p ◾* phomotopy.rfl = pwhisker_right f p := + idp ◾** !pwhisker_left_refl ⬝ !trans_refl + + definition pwhisker_left_trans {A B C : Type*} (g : B →* C) {f₁ f₂ f₃ : A →* B} + (p : f₁ ~* f₂) (q : f₂ ~* f₃) : + pwhisker_left g (p ⬝* q) = pwhisker_left g p ⬝* pwhisker_left g q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_left_refl⁻¹ ◾** !pwhisker_left_refl⁻¹, + refine ap (pwhisker_left g) !trans_refl ⬝ !pwhisker_left_refl ⬝ !trans_refl⁻¹ + end + + definition pwhisker_right_trans {A B C : Type*} (f : A →* B) {g₁ g₂ g₃ : B →* C} + (p : g₁ ~* g₂) (q : g₂ ~* g₃) : + pwhisker_right f (p ⬝* q) = pwhisker_right f p ⬝* pwhisker_right f q := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + refine _ ⬝ !pwhisker_right_refl⁻¹ ◾** !pwhisker_right_refl⁻¹, + refine ap (pwhisker_right f) !trans_refl ⬝ !pwhisker_right_refl ⬝ !trans_refl⁻¹ + end + + definition pwhisker_left_symm {A B C : Type*} (g : B →* C) {f₁ f₂ : A →* B} (p : f₁ ~* f₂) : + pwhisker_left g p⁻¹* = (pwhisker_left g p)⁻¹* := + begin + induction p using phomotopy_rec_on_idp, + refine _ ⬝ ap phomotopy.symm !pwhisker_left_refl⁻¹, + refine ap (pwhisker_left g) !refl_symm ⬝ !pwhisker_left_refl ⬝ !refl_symm⁻¹ + end + + definition pwhisker_right_symm {A B C : Type*} (f : A →* B) {g₁ g₂ : B →* C} (p : g₁ ~* g₂) : + pwhisker_right f p⁻¹* = (pwhisker_right f p)⁻¹* := + begin + induction p using phomotopy_rec_on_idp, + refine _ ⬝ ap phomotopy.symm !pwhisker_right_refl⁻¹, + refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹ + end + + definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := + idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans + + definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := + !refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s + + definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := + s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl + + definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := + !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + + definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q := + !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s + + definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q := + idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans + + definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q := + !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp + + definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} + {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p := + s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl + + section phsquare + /- + Squares of pointed homotopies + -/ + + variables {A B C : Type*} {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} + {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} + {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} + {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} + {p₀₃ : f₀₂ ~* f₀₄} {p₂₃ : f₂₂ ~* f₂₄} {p₄₃ : f₄₂ ~* f₄₄} + {p₁₄ : f₀₄ ~* f₂₄} {p₃₄ : f₂₄ ~* f₄₄} + + definition phsquare [reducible] (p₁₀ : f₀₀ ~* f₂₀) (p₁₂ : f₀₂ ~* f₂₂) + (p₀₁ : f₀₀ ~* f₀₂) (p₂₁ : f₂₀ ~* f₂₂) : Type := + p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ + + definition phsquare_of_eq (p : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := p + definition eq_of_phsquare (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : p₁₀ ⬝* p₂₁ = p₀₁ ⬝* p₁₂ := p + + -- definition phsquare.mk (p : Πx, square (p₁₀ x) (p₁₂ x) (p₀₁ x) (p₂₁ x)) + -- (q : cube (square_of_eq (to_homotopy_pt p₁₀)) (square_of_eq (to_homotopy_pt p₁₂)) + -- (square_of_eq (to_homotopy_pt p₀₁)) (square_of_eq (to_homotopy_pt p₂₁)) + -- (p pt) ids) : phsquare p₁₀ p₁₂ p₀₁ p₂₁ := + -- begin + -- fapply phomotopy_eq, + -- { intro x, apply eq_of_square (p x) }, + -- { generalize p pt, intro r, exact sorry } + -- end + + + definition phhconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₃₀ p₃₂ p₂₁ p₄₁) : + phsquare (p₁₀ ⬝* p₃₀) (p₁₂ ⬝* p₃₂) p₀₁ p₄₁ := + !trans_assoc ⬝ idp ◾** q ⬝ !trans_assoc⁻¹ ⬝ p ◾** idp ⬝ !trans_assoc + + definition phvconcat (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (q : phsquare p₁₂ p₁₄ p₀₃ p₂₃) : + phsquare p₁₀ p₁₄ (p₀₁ ⬝* p₀₃) (p₂₁ ⬝* p₂₃) := + (phhconcat p⁻¹ q⁻¹)⁻¹ + + definition phhdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare phomotopy.rfl phomotopy.rfl p₁ p₂ := + !refl_trans ⬝ q⁻¹ ⬝ !trans_refl⁻¹ + definition phvdeg_square {p₁ p₂ : f ~* f'} (q : p₁ = p₂) : phsquare p₁ p₂ phomotopy.rfl phomotopy.rfl := + !trans_refl ⬝ q ⬝ !refl_trans⁻¹ + + variables (p₀₁ p₁₀) + definition phhrefl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhdeg_square idp + definition phvrefl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvdeg_square idp + variables {p₀₁ p₁₀} + definition phhrfl : phsquare phomotopy.rfl phomotopy.rfl p₀₁ p₀₁ := phhrefl p₀₁ + definition phvrfl : phsquare p₁₀ p₁₀ phomotopy.rfl phomotopy.rfl := phvrefl p₁₀ + + /- + The names are very baroque. The following stands for + "pointed homotopy path-horizontal composition" (i.e. composition on the left with a path) + The names are obtained by using the ones for squares, and putting "ph" in front of it. + In practice, use the notation ⬝ph** defined below, which might be easier to remember + -/ + definition phphconcat {p₀₁'} (p : p₀₁' = p₀₁) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀ p₁₂ p₀₁' p₂₁ := + by induction p; exact q + + definition phhpconcat {p₂₁'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₂₁ = p₂₁') : + phsquare p₁₀ p₁₂ p₀₁ p₂₁' := + by induction p; exact q + + definition phpvconcat {p₁₀'} (p : p₁₀' = p₁₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀' p₁₂ p₀₁ p₂₁ := + by induction p; exact q + + definition phvpconcat {p₁₂'} (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) (p : p₁₂ = p₁₂') : + phsquare p₁₀ p₁₂' p₀₁ p₂₁ := + by induction p; exact q + + definition phhinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₀⁻¹* p₁₂⁻¹* p₂₁ p₀₁ := + begin + refine (eq_symm_trans_of_trans_eq _)⁻¹, + refine !trans_assoc⁻¹ ⬝ _, + refine (eq_trans_symm_of_trans_eq _)⁻¹, + exact (eq_of_phsquare p)⁻¹ + end + + definition phvinverse (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare p₁₂ p₁₀ p₀₁⁻¹* p₂₁⁻¹* := + (phhinverse p⁻¹)⁻¹ + + infix ` ⬝h** `:78 := phhconcat + infix ` ⬝v** `:78 := phvconcat + infixr ` ⬝ph** `:77 := phphconcat + infixl ` ⬝hp** `:77 := phhpconcat + infixr ` ⬝pv** `:77 := phpvconcat + infixl ` ⬝vp** `:77 := phvpconcat + postfix `⁻¹ʰ**`:(max+1) := phhinverse + postfix `⁻¹ᵛ**`:(max+1) := phvinverse + + definition phwhisker_rt (p : f ~* f₂₀) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (p₁₀ ⬝* p⁻¹*) p₁₂ p₀₁ (p ⬝* p₂₁) := + !trans_assoc ⬝ idp ◾** (!trans_assoc⁻¹ ⬝ !trans_left_inv ◾** idp ⬝ !refl_trans) ⬝ q + + definition phwhisker_br (p : f₂₂ ~* f) (q : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare p₁₀ (p₁₂ ⬝* p) p₀₁ (p₂₁ ⬝* p) := + !trans_assoc⁻¹ ⬝ q ◾** idp ⬝ !trans_assoc + + definition phmove_top_of_left' {p₀₁ : f ~* f₀₂} (p : f₀₀ ~* f) + (q : phsquare p₁₀ p₁₂ (p ⬝* p₀₁) p₂₁) : phsquare (p⁻¹* ⬝* p₁₀) p₁₂ p₀₁ p₂₁ := + !trans_assoc ⬝ (eq_symm_trans_of_trans_eq (q ⬝ !trans_assoc)⁻¹)⁻¹ + + definition phmove_bot_of_left {p₀₁ : f₀₀ ~* f} (p : f ~* f₀₂) + (q : phsquare p₁₀ p₁₂ (p₀₁ ⬝* p) p₂₁) : phsquare p₁₀ (p ⬝* p₁₂) p₀₁ p₂₁ := + q ⬝ !trans_assoc + + definition passoc_phomotopy_right {A B C D : Type*} (h : C →* D) (g : B →* C) {f f' : A →* B} + (p : f ~* f') : phsquare (passoc h g f) (passoc h g f') + (pwhisker_left (h ∘* g) p) (pwhisker_left h (pwhisker_left g p)) := + begin + induction p using phomotopy_rec_on_idp, + refine idp ◾** (ap (pwhisker_left h) !pwhisker_left_refl ⬝ !pwhisker_left_refl) ⬝ _ ⬝ + !pwhisker_left_refl⁻¹ ◾** idp, + exact !trans_refl ⬝ !refl_trans⁻¹ + end + + theorem passoc_phomotopy_middle {A B C D : Type*} (h : C →* D) {g g' : B →* C} (f : A →* B) + (p : g ~* g') : phsquare (passoc h g f) (passoc h g' f) + (pwhisker_right f (pwhisker_left h p)) (pwhisker_left h (pwhisker_right f p)) := + begin + induction p using phomotopy_rec_on_idp, + rewrite [pwhisker_right_refl, pwhisker_left_refl], + rewrite [pwhisker_right_refl, pwhisker_left_refl], + exact phvrfl + end + + definition pwhisker_right_pwhisker_left {A B C : Type*} {g g' : B →* C} {f f' : A →* B} + (p : g ~* g') (q : f ~* f') : + phsquare (pwhisker_right f p) (pwhisker_right f' p) (pwhisker_left g q) (pwhisker_left g' q) := + begin + induction p using phomotopy_rec_on_idp, + induction q using phomotopy_rec_on_idp, + exact !pwhisker_right_refl ◾** !pwhisker_left_refl ⬝ + !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ + end + + definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂) + (pwhisker_left f p₀₁) (pwhisker_left f p₂₁) := + !pwhisker_left_trans⁻¹ ⬝ ap (pwhisker_left f) p ⬝ !pwhisker_left_trans + + definition pwhisker_right_phsquare (f : C →* A) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : + phsquare (pwhisker_right f p₁₀) (pwhisker_right f p₁₂) + (pwhisker_right f p₀₁) (pwhisker_right f p₂₁) := + !pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans + + end phsquare + + definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : + phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := + begin induction q, induction p, exact !trans_refl⁻¹ end + + definition pcompose_left_eq_of_phomotopy {A B C : Type*} (g : B →* C) {f f' : A →* B} + (H : f ~* f') : ap (λf, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_left g H) := + begin + induction H using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !pwhisker_left_refl⁻¹ + end + + definition pcompose_right_eq_of_phomotopy {A B C : Type*} {g g' : B →* C} (f : A →* B) + (H : g ~* g') : ap (λg, g ∘* f) (eq_of_phomotopy H) = eq_of_phomotopy (pwhisker_right f H) := + begin + induction H using phomotopy_rec_on_idp, + refine ap02 _ !eq_of_phomotopy_refl ⬝ !eq_of_phomotopy_refl⁻¹ ⬝ ap eq_of_phomotopy _, + exact !pwhisker_right_refl⁻¹ + end + + definition phomotopy_of_eq_pcompose_left {A B C : Type*} (g : B →* C) {f f' : A →* B} + (p : f = f') : phomotopy_of_eq (ap (λf, g ∘* f) p) = pwhisker_left g (phomotopy_of_eq p) := + begin + induction p, exact !pwhisker_left_refl⁻¹ + end + + definition phomotopy_of_eq_pcompose_right {A B C : Type*} {g g' : B →* C} (f : A →* B) + (p : g = g') : phomotopy_of_eq (ap (λg, g ∘* f) p) = pwhisker_right f (phomotopy_of_eq p) := + begin + induction p, exact !pwhisker_right_refl⁻¹ + end + + definition phomotopy_mk_ppmap [constructor] {A B C : Type*} {f g : A →* ppmap B C} (p : Πa, f a ~* g a) + (q : p pt ⬝* phomotopy_of_eq (respect_pt g) = phomotopy_of_eq (respect_pt f)) + : 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], + refine !phomotopy_of_eq_con ⬝ _, + refine !phomotopy_of_eq_of_phomotopy ◾** idp ⬝ q, + end + + definition pconst_pcompose_pconst (A B C : Type*) : + pconst_pcompose (pconst A B) = pcompose_pconst (pconst B C) := + idp + + definition pconst_pcompose_phomotopy_pconst {A B C : Type*} {f : A →* B} (p : f ~* pconst A B) : + pconst_pcompose f = pwhisker_left (pconst B C) p ⬝* pcompose_pconst (pconst B C) := + begin + assert H : Π(p : pconst A B ~* f), + pconst_pcompose f = pwhisker_left (pconst B C) p⁻¹* ⬝* pcompose_pconst (pconst B C), + { intro p, induction p using phomotopy_rec_on_idp, reflexivity }, + refine H p⁻¹* ⬝ ap (pwhisker_left _) !symm_symm ◾** idp, + end + + definition passoc_pconst_right {A B C D : Type*} (h : C →* D) (g : B →* C) : + passoc h g (pconst A B) ⬝* (pwhisker_left h (pcompose_pconst g) ⬝* pcompose_pconst h) = + pcompose_pconst (h ∘* g) := + begin + fapply phomotopy_eq, + { intro a, exact !idp_con }, + { induction h with h h₀, induction g with g g₀, induction D with D d₀, induction C with C c₀, + esimp at *, induction g₀, induction h₀, reflexivity } + end + + definition passoc_pconst_middle {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : + passoc g (pconst A B) f ⬝* (pwhisker_left g (pconst_pcompose f) ⬝* pcompose_pconst g) = + pwhisker_right f (pcompose_pconst g) ⬝* pconst_pcompose f := + begin + fapply phomotopy_eq, + { intro a, exact !idp_con ⬝ !idp_con }, + { induction g with g g₀, induction f with f f₀, induction B' with D d₀, induction A with C c₀, + esimp at *, induction g₀, induction f₀, reflexivity } + end + + definition passoc_pconst_left {A B C D : Type*} (g : B →* C) (f : A →* B) : + phsquare (passoc (pconst C D) g f) (pconst_pcompose f) + (pwhisker_right f (pconst_pcompose g)) (pconst_pcompose (g ∘* f)) := + begin + fapply phomotopy_eq, + { intro a, exact !idp_con }, + { induction g with g g₀, induction f with f f₀, induction C with C c₀, induction B with B b₀, + esimp at *, induction g₀, induction f₀, reflexivity } + end + + definition ppcompose_left_pcompose [constructor] {A B C D : Type*} (h : C →* D) (g : B →* C) : + @ppcompose_left A _ _ (h ∘* g) ~* ppcompose_left h ∘* ppcompose_left g := + begin + fapply phomotopy_mk_ppmap, + { exact passoc h g }, + { refine idp ◾** (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + exact passoc_pconst_right h g } + end + + definition ppcompose_right_pcompose [constructor] {A B C D : Type*} (g : B →* C) (f : A →* B) : + @ppcompose_right _ _ D (g ∘* f) ~* ppcompose_right f ∘* ppcompose_right g := + begin + symmetry, + fapply phomotopy_mk_ppmap, + { intro h, exact passoc h g f }, + { refine idp ◾** !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** !phomotopy_of_eq_of_phomotopy)⁻¹, + exact passoc_pconst_left g f } + end + + definition ppcompose_left_ppcompose_right {A A' B B' : Type*} (g : B →* B') (f : A' →* A) : + psquare (ppcompose_left g) (ppcompose_left g) (ppcompose_right f) (ppcompose_right f) := + begin + fapply phomotopy_mk_ppmap, + { intro h, exact passoc g h f }, + { refine idp ◾** (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_left_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (!phomotopy_of_eq_con ⬝ + (ap phomotopy_of_eq !pcompose_right_eq_of_phomotopy ⬝ !phomotopy_of_eq_of_phomotopy) ◾** + !phomotopy_of_eq_of_phomotopy)⁻¹, + apply passoc_pconst_middle } + end + + definition pcompose_pconst_phomotopy {A B C : Type*} {f f' : B →* C} (p : f ~* f') : + pwhisker_right (pconst A B) p ⬝* pcompose_pconst f' = pcompose_pconst f := + begin + fapply phomotopy_eq, + { intro a, exact to_homotopy_pt p }, + { induction p using phomotopy_rec_on_idp, induction C with C c₀, induction f with f f₀, + esimp at *, induction f₀, reflexivity } + end + + definition pid_pconst (A B : Type*) : pcompose_pconst (pid B) = pid_pcompose (pconst A B) := + by reflexivity + + definition pid_pconst_pcompose {A B C : Type*} (f : A →* B) : + phsquare (pid_pcompose (pconst B C ∘* f)) + (pcompose_pconst (pid C)) + (pwhisker_left (pid C) (pconst_pcompose f)) + (pconst_pcompose f) := + begin + fapply phomotopy_eq, + { reflexivity }, + { induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, reflexivity } + end + + definition ppcompose_left_pconst [constructor] (A B C : Type*) : + @ppcompose_left A _ _ (pconst B C) ~* pconst (ppmap A B) (ppmap A C) := + begin + fapply phomotopy_mk_ppmap, + { exact pconst_pcompose }, + { refine idp ◾** !phomotopy_of_eq_idp ⬝ !phomotopy_of_eq_of_phomotopy⁻¹ } + end + + definition ppcompose_left_phomotopy [constructor] {A B C : Type*} {g g' : B →* C} (p : g ~* g') : + @ppcompose_left A _ _ g ~* ppcompose_left g' := + begin + induction p using phomotopy_rec_on_idp, + reflexivity + end + + definition ppcompose_left_phomotopy_refl {A B C : Type*} (g : B →* C) : + ppcompose_left_phomotopy (phomotopy.refl g) = phomotopy.refl (@ppcompose_left A _ _ g) := + !phomotopy_rec_on_idp_refl + + /- a more explicit proof of ppcompose_left_phomotopy, which might be useful if we need to prove properties about it + -/ + -- fapply phomotopy_mk_ppmap, + -- { intro f, exact pwhisker_right f p }, + -- { refine ap (λx, _ ⬝* x) !phomotopy_of_eq_of_phomotopy ⬝ _ ⬝ !phomotopy_of_eq_of_phomotopy⁻¹, + -- exact pcompose_pconst_phomotopy p } + + definition ppcompose_right_phomotopy [constructor] {A B C : Type*} {f f' : A →* B} (p : f ~* f') : + @ppcompose_right _ _ C f ~* ppcompose_right f' := + begin + induction p using phomotopy_rec_on_idp, + reflexivity + end + + definition pppcompose [constructor] (A B C : Type*) : ppmap B C →* ppmap (ppmap A B) (ppmap A C) := + pmap.mk ppcompose_left (eq_of_phomotopy !ppcompose_left_pconst) + + section psquare + + variables {A A' A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type*} + {f₁₀ f₁₀' : A₀₀ →* A₂₀} {f₃₀ : A₂₀ →* A₄₀} + {f₀₁ f₀₁' : A₀₀ →* A₀₂} {f₂₁ f₂₁' : A₂₀ →* A₂₂} {f₄₁ : A₄₀ →* A₄₂} + {f₁₂ f₁₂' : A₀₂ →* A₂₂} {f₃₂ : A₂₂ →* A₄₂} + {f₀₃ : A₀₂ →* A₀₄} {f₂₃ : A₂₂ →* A₂₄} {f₄₃ : A₄₂ →* A₄₄} + {f₁₄ : A₀₄ →* A₂₄} {f₃₄ : A₂₄ →* A₄₄} + + definition ppcompose_left_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (@ppcompose_left A _ _ f₁₀) (ppcompose_left f₁₂) + (ppcompose_left f₀₁) (ppcompose_left f₂₁) := + !ppcompose_left_pcompose⁻¹* ⬝* ppcompose_left_phomotopy p ⬝* !ppcompose_left_pcompose + + definition ppcompose_right_psquare {A : Type*} (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + psquare (@ppcompose_right _ _ A f₁₂) (ppcompose_right f₁₀) + (ppcompose_right f₂₁) (ppcompose_right f₀₁) := + !ppcompose_right_pcompose⁻¹* ⬝* ppcompose_right_phomotopy p⁻¹* ⬝* !ppcompose_right_pcompose + + definition trans_phomotopy_hconcat {f₀₁' f₀₁''} + (q₂ : f₀₁'' ~* f₀₁') (q₁ : f₀₁' ~* f₀₁) (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : + (q₂ ⬝* q₁) ⬝ph* p = q₂ ⬝ph* q₁ ⬝ph* p := + idp ◾** (ap (pwhisker_left f₁₂) !trans_symm ⬝ !pwhisker_left_trans) ⬝ !trans_assoc⁻¹ + + definition symm_phomotopy_hconcat {f₀₁'} (q : f₀₁ ~* f₀₁') + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : q⁻¹* ⬝ph* p = p ⬝* pwhisker_left f₁₂ q := + idp ◾** ap (pwhisker_left f₁₂) !symm_symm + + definition refl_phomotopy_hconcat (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) : phomotopy.rfl ⬝ph* p = p := + idp ◾** (ap (pwhisker_left _) !refl_symm ⬝ !pwhisker_left_refl) ⬝ !trans_refl + + local attribute phomotopy.rfl [reducible] + theorem pwhisker_left_phomotopy_hconcat {f₀₁'} (r : f₀₁' ~* f₀₁) + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + pwhisker_left f₀₃ r ⬝ph* (p ⬝v* q) = (r ⬝ph* p) ⬝v* q := + by induction r using phomotopy_rec_on_idp; rewrite [pwhisker_left_refl, +refl_phomotopy_hconcat] + + theorem pvcompose_pwhisker_left {f₀₁'} (r : f₀₁ ~* f₀₁') + (p : psquare f₁₀ f₁₂ f₀₁ f₂₁) (q : psquare f₁₂ f₁₄ f₀₃ f₂₃) : + (p ⬝v* q) ⬝* (pwhisker_left f₁₄ (pwhisker_left f₀₃ r)) = (p ⬝* pwhisker_left f₁₂ r) ⬝v* q := + by induction r using phomotopy_rec_on_idp; rewrite [+pwhisker_left_refl, + trans_refl] + + definition phconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₃₀ f₃₂ f₂₁ f₄₁} + (r : p = p') (s : q = q') : p ⬝h* q = p' ⬝h* q' := + ap011 phconcat r s + + definition pvconcat2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : psquare f₁₂ f₁₄ f₀₃ f₂₃} + (r : p = p') (s : q = q') : p ⬝v* q = p' ⬝v* q' := + ap011 pvconcat r s + + definition phinverse2 {f₁₀ : A₀₀ ≃* A₂₀} {f₁₂ : A₀₂ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : p = p') : p⁻¹ʰ* = p'⁻¹ʰ* := + ap phinverse r + + definition pvinverse2 {f₀₁ : A₀₀ ≃* A₀₂} {f₂₁ : A₂₀ ≃* A₂₂} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : p = p') : p⁻¹ᵛ* = p'⁻¹ᵛ* := + ap pvinverse r + + definition phomotopy_hconcat2 {q q' : f₀₁' ~* f₀₁} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : q = q') (s : p = p') : q ⬝ph* p = q' ⬝ph* p' := + ap011 phomotopy_hconcat r s + + definition hconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₂₁' ~* f₂₁} + (r : p = p') (s : q = q') : p ⬝hp* q = p' ⬝hp* q' := + ap011 hconcat_phomotopy r s + + definition phomotopy_vconcat2 {q q' : f₁₀' ~* f₁₀} {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} + (r : q = q') (s : p = p') : q ⬝pv* p = q' ⬝pv* p' := + ap011 phomotopy_vconcat r s + + definition vconcat_phomotopy2 {p p' : psquare f₁₀ f₁₂ f₀₁ f₂₁} {q q' : f₁₂' ~* f₁₂} + (r : p = p') (s : q = q') : p ⬝vp* q = p' ⬝vp* q' := + ap011 vconcat_phomotopy r s + + -- for consistency, should there be a second star here? + infix ` ◾h* `:79 := phconcat2 + infix ` ◾v* `:79 := pvconcat2 + infixl ` ◾hp* `:79 := hconcat_phomotopy2 + infixr ` ◾ph* `:79 := phomotopy_hconcat2 + infixl ` ◾vp* `:79 := vconcat_phomotopy2 + infixr ` ◾pv* `:79 := phomotopy_vconcat2 + postfix `⁻²ʰ*`:(max+1) := phinverse2 + postfix `⁻²ᵛ*`:(max+1) := pvinverse2 + + end psquare + + variables {X X' Y Y' Z : Type*} + definition pap1 [constructor] (X Y : Type*) : ppmap X Y →* ppmap (Ω X) (Ω Y) := + pmap.mk ap1 (eq_of_phomotopy !ap1_pconst) + + definition ap1_gen_const {A B : Type} {a₁ a₂ : A} (b : B) (p : a₁ = a₂) : + ap1_gen (const A b) idp idp p = idp := + ap1_gen_idp_left (const A b) p ⬝ ap_constant p b + + definition ap1_gen_compose_const_left + {A B C : Type} (c : C) (f : A → B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose (const B c) f idp idp idp idp p ⬝ + ap1_gen_const c (ap1_gen f idp idp p) = + ap1_gen_const c p := + begin induction p, reflexivity end + + definition ap1_gen_compose_const_right + {A B C : Type} (g : B → C) (b : B) {a₁ a₂ : A} (p : a₁ = a₂) : + ap1_gen_compose g (const A b) idp idp idp idp p ⬝ + ap (ap1_gen g idp idp) (ap1_gen_const b p) = + ap1_gen_const (g b) p := + begin induction p, reflexivity end + + definition ap1_pcompose_pconst_left {A B C : Type*} (f : A →* B) : + phsquare (ap1_pcompose (pconst B C) f) + (ap1_pconst A C) + (ap1_phomotopy (pconst_pcompose f)) + (pwhisker_right (Ω→ f) (ap1_pconst B C) ⬝* pconst_pcompose (Ω→ f)) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, induction f with f f₀, + esimp at *, induction f₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_left c₀ f }, + { reflexivity } + end + + definition ap1_pcompose_pconst_right {A B C : Type*} (g : B →* C) : + phsquare (ap1_pcompose g (pconst A B)) + (ap1_pconst A C) + (ap1_phomotopy (pcompose_pconst g)) + (pwhisker_left (Ω→ g) (ap1_pconst A B) ⬝* pcompose_pconst (Ω→ g)) := + begin + induction A with A a₀, induction B with B b₀, induction C with C c₀, induction g with g g₀, + esimp at *, induction g₀, + refine idp ◾** !trans_refl ⬝ _ ⬝ !refl_trans⁻¹ ⬝ !ap1_phomotopy_refl⁻¹ ◾** idp, + fapply phomotopy_eq, + { exact ap1_gen_compose_const_right g b₀ }, + { reflexivity } + end + + definition pap1_natural_left [constructor] (f : X' →* X) : + psquare (pap1 X Y) (pap1 X' Y) (ppcompose_right f) (ppcompose_right (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_right_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_left f)⁻¹ } + end + + definition pap1_natural_right [constructor] (f : Y →* Y') : + psquare (pap1 X Y) (pap1 X Y') (ppcompose_left f) (ppcompose_left (Ω→ f)) := + begin + fapply phomotopy_mk_ppmap, + { intro g, exact !ap1_pcompose⁻¹* }, + { refine idp ◾** (ap phomotopy_of_eq (!ap1_eq_of_phomotopy ◾ idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ + !phomotopy_of_eq_of_phomotopy) ⬝ _ ⬝ (ap phomotopy_of_eq (!pcompose_left_eq_of_phomotopy ◾ + idp ⬝ !eq_of_phomotopy_trans⁻¹) ⬝ !phomotopy_of_eq_of_phomotopy)⁻¹, + apply symm_trans_eq_of_eq_trans, exact (ap1_pcompose_pconst_right f)⁻¹ } + end + +end pointed diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 595e82881..f3c8217e5 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -90,6 +90,29 @@ namespace prod definition ap_prod_mk_right (p : b = b') : ap (λb, prod.mk a b) p = prod_eq idp p := ap_eq_ap011_right prod.mk a p + definition pair_eq_eta {A B : Type} {u v : A × B} + (p : u = v) : pair_eq (p..1) (p..2) = prod.eta u ⬝ p ⬝ (prod.eta v)⁻¹ := + by induction p; induction u; reflexivity + + definition prod_eq_eq {A B : Type} {u v : A × B} + {p₁ q₁ : u.1 = v.1} {p₂ q₂ : u.2 = v.2} (α₁ : p₁ = q₁) (α₂ : p₂ = q₂) + : prod_eq p₁ p₂ = prod_eq q₁ q₂ := + by cases α₁; cases α₂; reflexivity + + definition prod_eq_assemble {A B : Type} {u v : A × B} + {p q : u = v} (α₁ : p..1 = q..1) (α₂ : p..2 = q..2) : p = q := + (prod_eq_eta p)⁻¹ ⬝ prod.prod_eq_eq α₁ α₂ ⬝ prod_eq_eta q + + definition eq_pr1_concat {A B : Type} {u v w : A × B} + (p : u = v) (q : v = w) + : (p ⬝ q)..1 = p..1 ⬝ q..1 := + by cases q; reflexivity + + definition eq_pr2_concat {A B : Type} {u v w : A × B} + (p : u = v) (q : v = w) + : (p ⬝ q)..2 = p..2 ⬝ q..2 := + by cases q; reflexivity + /- Groupoid structure -/ definition prod_eq_inv (p : a = a') (q : b = b') : (prod_eq p q)⁻¹ = prod_eq p⁻¹ q⁻¹ := by cases p; cases q; reflexivity @@ -125,6 +148,19 @@ namespace prod apply idpo end + open prod.ops + definition prod_pathover_equiv {A : Type} {B C : A → Type} {a a' : A} (p : a = a') + (x : B a × C a) (x' : B a' × C a') : x =[p] x' ≃ x.1 =[p] x'.1 × x.2 =[p] x'.2 := + begin + fapply equiv.MK, + { intro q, induction q, constructor: constructor }, + { intro v, induction v with q r, exact prod_pathover _ _ _ q r }, + { intro v, induction v with q r, induction x with b c, induction x' with b' c', + esimp at *, induction q, refine idp_rec_on r _, reflexivity }, + { intro q, induction q, induction x with b c, reflexivity } + end + + /- TODO: * define the projections from the type u =[p] v @@ -301,6 +337,8 @@ namespace prod definition ptprod [constructor] {n : ℕ₋₂} (A B : n-Type*) : n-Type* := ptrunctype.mk' n (A × B) + definition pprod_functor [constructor] {A B C D : Type*} (f : A →* C) (g : B →* D) : A ×* B →* C ×* D := + pmap.mk (prod_functor f g) (prod_eq (respect_pt f) (respect_pt g)) end prod diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 2fca3c659..e0a26e996 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -214,6 +214,25 @@ namespace sigma induction s using idp_rec_on, apply idpo end + definition pathover_pr1 [unfold 9] {A : Type} {B : A → Type} {C : Πa, B a → Type} + {a a' : A} {p : a = a'} {x : Σb, C a b} {x' : Σb', C a' b'} + (q : x =[p] x') : x.1 =[p] x'.1 := + begin induction q, constructor end + + definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} (C : Πa, B a → Type) + {a a' : A} (p : a = a') (x : Σb, C a b) (x' : Σb', C a' b') + [Πa b, is_prop (C a b)] : x =[p] x' ≃ x.1 =[p] x'.1 := + begin + fapply equiv.MK, + { exact pathover_pr1 }, + { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q, + apply pathover_idp_of_eq, exact sigma_eq idp !is_prop.elimo }, + { intro q, induction x with b c, induction x' with b' c', esimp at q, induction q, + have c = c', from !is_prop.elim, induction this, + rewrite [▸*, is_prop_elimo_self (C a) c] }, + { intro q, induction q, induction x with b c, rewrite [▸*, is_prop_elimo_self (C a) c] } + end + /- TODO: * define the projections from the type u =[p] v @@ -274,6 +293,10 @@ namespace sigma ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover.rec_on q idpo) := by induction q; reflexivity + definition sigma_ua {A B : Type} (C : A ≃ B → Type) : + (Σ(p : A = B), C (equiv_of_eq p)) ≃ Σ(e : A ≃ B), C e := + sigma_equiv_sigma_left' !eq_equiv_equiv + -- definition ap_sigma_functor_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) -- : ap (sigma_functor f g) (sigma_eq p q) = -- sigma_eq (ap f p) @@ -511,7 +534,6 @@ namespace sigma (b : B a) (b' : B a') : a = a' := (is_prop.elim ⟨a, b⟩ ⟨a', b'⟩)..1 - end sigma attribute sigma.is_trunc_sigma [instance] [priority 1490] diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 77c0e6d27..bcce386a0 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -8,10 +8,10 @@ Properties of trunc_index, is_trunc, trunctype, trunc, and the pointed versions -- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc -import .pointed ..function algebra.order types.nat.order +import .pointed ..function algebra.order types.nat.order types.unit open eq sigma sigma.ops pi function equiv trunctype - is_equiv prod pointed nat is_trunc algebra sum + is_equiv prod pointed nat is_trunc algebra sum unit /- basic computation with ℕ₋₂, its operations and its order -/ namespace trunc_index @@ -471,6 +471,22 @@ namespace is_trunc have is_trunc (0+[ℕ₋₂]n) A, by rewrite [trunc_index.zero_add]; exact _, is_trunc_loopn 0 n A + definition pequiv_punit_of_is_contr [constructor] (A : Type*) (H : is_contr A) : A ≃* punit := + pequiv_of_equiv (equiv_unit_of_is_contr A) (@is_prop.elim unit _ _ _) + + definition pequiv_punit_of_is_contr' [constructor] (A : Type) (H : is_contr A) + : pointed.MK A (center A) ≃* punit := + pequiv_punit_of_is_contr (pointed.MK A (center A)) H + + definition is_trunc_is_contr_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) + (b : B) [is_trunc n A] [is_trunc n B] : is_trunc n (is_contr (fiber f b)) := + begin + cases n, + { apply is_contr_of_inhabited_prop, apply is_contr_fun_of_is_equiv, + apply is_equiv_of_is_contr }, + { apply is_trunc_succ_of_is_prop } + end + end is_trunc open is_trunc namespace trunc @@ -735,9 +751,10 @@ namespace trunc revert n, induction k with k IH: intro n, { reflexivity}, { refine _ ⬝e* loop_ptrunc_pequiv n (Ω[k] A), - rewrite [loopn_succ_eq], apply loop_pequiv_loop, + change Ω (Ω[k] (ptrunc (n + succ k) A)) ≃* Ω (ptrunc (n + 1) (Ω[k] A)), + apply loop_pequiv_loop, refine _ ⬝e* IH (n.+1), - rewrite succ_add_nat} + exact loopn_pequiv_loopn k (pequiv_of_eq (ap (λn, ptrunc n A) !succ_add_nat⁻¹)) } end definition loopn_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*} diff --git a/hott/types/types.md b/hott/types/types.md index 4da764298..5a41393c7 100644 --- a/hott/types/types.md +++ b/hott/types/types.md @@ -30,4 +30,5 @@ Types in HoTT: * [trunc](trunc.hlean): truncation levels, n-types, truncation * [pullback](pullback.hlean) * [univ](univ.hlean) -* [type_functor](type_functor.hlean) \ No newline at end of file +* [type_functor](type_functor.hlean) +* [pointed2](pointed2.hlean): equalities between pointed homotopies, squares of poitned maps and pointed homotopies, and pointed maps in or out of `ppmap A B`