diff --git a/hott/algebra/bundled.hlean b/hott/algebra/bundled.hlean index 8f42b2185..69eaea99e 100644 --- a/hott/algebra/bundled.hlean +++ b/hott/algebra/bundled.hlean @@ -33,45 +33,37 @@ structure CommMonoid := attribute CommMonoid.carrier [coercion] attribute CommMonoid.struct [instance] -abbreviation signature := interval -structure Group (i : signature) := +structure Group := (carrier : Type) (struct : group carrier) -definition MulGroup : Type := Group interval.zero -definition AddGroup : Type := Group interval.one attribute Group.carrier [coercion] -definition MulGroup.mk [constructor] [reducible] (G : Type) (H : group G) : MulGroup := -Group.mk _ G _ +definition AddGroup : Type := Group + definition AddGroup.mk [constructor] [reducible] (G : Type) (H : add_group G) : AddGroup := -Group.mk _ G add_group.to_group +Group.mk G H -definition MulGroup.struct [reducible] (G : MulGroup) : group G := Group.struct G definition AddGroup.struct [reducible] (G : AddGroup) : add_group G := -@group.to_add_group _ (Group.struct G) +Group.struct G -attribute MulGroup.struct AddGroup.struct [instance] [priority 2000] -attribute Group.struct [instance] [priority 800] +attribute AddGroup.struct Group.struct [instance] [priority 2000] -structure CommGroup (i : signature) := +structure CommGroup := (carrier : Type) (struct : comm_group carrier) -definition MulCommGroup : Type := CommGroup interval.zero -definition AddCommGroup : Type := CommGroup interval.one attribute CommGroup.carrier [coercion] -definition MulCommGroup.mk [constructor] [reducible] (G : Type) (H : comm_group G) : MulCommGroup := -CommGroup.mk _ G _ +definition AddCommGroup : Type := CommGroup + definition AddCommGroup.mk [constructor] [reducible] (G : Type) (H : add_comm_group G) : AddCommGroup := -CommGroup.mk _ G add_comm_group.to_comm_group +CommGroup.mk G H -definition MulCommGroup.struct [reducible] (G : MulCommGroup) : comm_group G := CommGroup.struct G definition AddCommGroup.struct [reducible] (G : AddCommGroup) : add_comm_group G := -@comm_group.to_add_comm_group _ (CommGroup.struct G) +CommGroup.struct G + +attribute AddCommGroup.struct CommGroup.struct [instance] [priority 2000] -attribute MulCommGroup.struct AddCommGroup.struct [instance] [priority 2000] -attribute CommGroup.struct [instance] [priority 800] -- structure AddSemigroup := -- (carrier : Type) (struct : add_semigroup carrier) diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index a1e14f402..e7b0a7421 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -79,7 +79,7 @@ namespace category definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C := Groupoid.rec (λob c, idp) C - definition Groupoid_of_Group [constructor] {i : signature} (G : Group i) : Groupoid := + definition Groupoid_of_Group [constructor] (G : Group) : Groupoid := Groupoid.mk unit (groupoid_of_group G) end category diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index c067d8aca..0d8447579 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -15,21 +15,20 @@ open eq algebra pointed function is_trunc pi category equiv is_equiv set_option class.force_new true namespace group - definition pointed_Group [instance] [constructor] {i : signature} (G : Group i) : pointed G := + definition pointed_Group [instance] [constructor] (G : Group) : pointed G := pointed.mk 1 - definition pType_of_Group [constructor] [reducible] {i : signature} (G : Group i) : Type* := + definition pType_of_Group [constructor] [reducible] (G : Group) : Type* := pointed.MK G 1 - definition Set_of_Group [constructor] {i : signature} (G : Group i) : Set := trunctype.mk G _ + definition Set_of_Group [constructor] (G : Group) : Set := trunctype.mk G _ - definition Group_of_CommGroup [coercion] [constructor] {i : signature} (G : CommGroup i) : - Group i := - Group.mk i G _ + definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := + Group.mk G _ definition comm_group_Group_of_CommGroup [instance] [constructor] [priority 900] - {i : signature} (G : CommGroup i) : comm_group (Group_of_CommGroup G) := + (G : CommGroup) : comm_group (Group_of_CommGroup G) := begin esimp, exact _ end - definition group_pType_of_Group [instance] [priority 900] {i : signature} (G : Group i) : + definition group_pType_of_Group [instance] [priority 900] (G : Group) : group (pType_of_Group G) := Group.struct G @@ -100,19 +99,18 @@ namespace group end additive - structure homomorphism {i j : signature} (G₁ : Group i) (G₂ : Group j) : Type := + structure homomorphism (G₁ G₂ : Group) : Type := (φ : G₁ → G₂) (p : is_homomorphism φ) infix ` →g `:55 := homomorphism - definition group_fun [unfold 5] [coercion] := @homomorphism.φ - definition homomorphism.struct [instance] [priority 900] {i j : signature} - {G₁ : Group i} {G₂ : Group j} (φ : G₁ →g G₂) + definition group_fun [unfold 3] [coercion] := @homomorphism.φ + definition homomorphism.struct [instance] [priority 900] {G₁ : Group} {G₂ : Group} (φ : G₁ →g G₂) : is_homomorphism φ := homomorphism.p φ - definition homomorphism.mulstruct [instance] [priority 2000] {G₁ G₂ : MulGroup } (φ : G₁ →g G₂) + definition homomorphism.mulstruct [instance] [priority 2000] {G₁ G₂ : Group } (φ : G₁ →g G₂) : is_homomorphism φ := homomorphism.p φ @@ -120,8 +118,7 @@ namespace group : is_add_homomorphism φ := homomorphism.p φ - variables {i j k l : signature} {G : Group i} {G₁ : Group j} {G₂ : Group k} {G₃ : Group l} - {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂) + variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂) definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h := respect_mul φ g h @@ -173,7 +170,7 @@ namespace group end additive section add_mul - variables {H₁ : AddGroup} {H₂ : Group i} (χ : H₁ →g H₂) + variables {H₁ : AddGroup} {H₂ : Group} (χ : H₁ →g H₂) definition to_respect_add_mul /- χ -/ (g h : H₁) : χ (g + h) = χ g * χ h := to_respect_mul χ g h @@ -186,7 +183,7 @@ namespace group end add_mul section mul_add - variables {H₁ : Group i} {H₂ : AddGroup} (χ : H₁ →g H₂) + variables {H₁ : Group} {H₂ : AddGroup} (χ : H₁ →g H₂) definition to_respect_mul_add /- χ -/ (g h : H₁) : χ (g * h) = χ g + χ h := to_respect_mul χ g h @@ -211,7 +208,7 @@ namespace group infixr ` ∘g `:75 := homomorphism_compose notation 1 := homomorphism_id _ - structure isomorphism {i j : signature} (A : Group i) (B : Group j) := + structure isomorphism (A B : Group) := (to_hom : A →g B) (is_equiv_to_hom : is_equiv to_hom) @@ -230,10 +227,10 @@ namespace group (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ := isomorphism.mk (homomorphism.mk φ p) !to_is_equiv - definition eq_of_isomorphism {G₁ G₂ : Group i} (φ : G₁ ≃g G₂) : G₁ = G₂ := + definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ := Group_eq (equiv_of_isomorphism φ) (respect_mul φ) - definition isomorphism_of_eq {G₁ G₂ : Group i} (φ : G₁ = G₂) : G₁ ≃g G₂ := + definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ := isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ)) begin intros, induction φ, reflexivity end @@ -256,11 +253,11 @@ namespace group isomorphism.mk (ψ ∘g φ) !is_equiv_compose definition isomorphism.eq_trans [trans] [constructor] - {G₁ G₂ : Group i} {G₃ : Group j} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := + {G₁ G₂ : Group} {G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ := proof isomorphism.trans (isomorphism_of_eq φ) ψ qed definition isomorphism.trans_eq [trans] [constructor] - {G₁ : Group i} {G₂ G₃ : Group j} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ := + {G₁ : Group} {G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ := isomorphism.trans φ (isomorphism_of_eq ψ) postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm @@ -280,10 +277,10 @@ namespace group /- category of groups -/ - definition precategory_group [constructor] (i : signature) : precategory (Group i) := + definition precategory_group [constructor] : precategory Group := precategory.mk homomorphism - (@homomorphism_compose _ _ _) - (@homomorphism_id _) + @homomorphism_compose + @homomorphism_id (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp)) (λG₁ G₂ φ, homomorphism_eq (λg, idp)) (λG₁ G₂ φ, homomorphism_eq (λg, idp)) @@ -349,7 +346,7 @@ namespace group { intros, reflexivity} end - definition trivial_group_of_is_contr' (G : MulGroup) [H : is_contr G] : G = G0 := + definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 := eq_of_isomorphism (trivial_group_of_is_contr G) variable {G} diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index dff58db36..c35485594 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -36,13 +36,13 @@ namespace eq local attribute comm_group_homotopy_group [instance] - definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulGroup := - MulGroup.mk (π[succ n] A) _ + definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : Group := + Group.mk (π[succ n] A) _ - definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulCommGroup := - MulCommGroup.mk (π[succ (succ n)] A) _ + definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup := + CommGroup.mk (π[succ (succ n)] A) _ - definition fundamental_group [constructor] (A : Type*) : MulGroup := + definition fundamental_group [constructor] (A : Type*) : Group := ghomotopy_group zero A notation `πg[`:95 n:0 ` +1]`:0 := ghomotopy_group n @@ -249,7 +249,6 @@ namespace eq -- loop_space_succ_eq_in_concat, - + tr_compose], -- end - local attribute MulGroup MulCommGroup [reducible] definition is_homomorphism_inverse (A : Type*) (n : ℕ) : is_homomorphism (λp, p⁻¹ : (πag[n+2] A) → (πag[n+2] A)) := begin diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 2e0a60659..1df2fa626 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -15,8 +15,8 @@ namespace algebra definition trivial_group [constructor] : group unit := group.mk (λx y, star) _ (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) - definition Trivial_group [constructor] : MulGroup := - MulGroup.mk _ trivial_group + definition Trivial_group [constructor] : Group := + Group.mk _ trivial_group abbreviation G0 := Trivial_group @@ -65,15 +65,15 @@ namespace algebra apply pathover_idp_of_eq, exact group_eq (resp_mul) end - definition Group_eq_of_eq {i : signature} {G H : Group i} (p : carrier G = carrier H) + definition Group_eq_of_eq {G H : Group} (p : carrier G = carrier H) (resp_mul : Π(g h : G), cast p (g * h) = cast p g * cast p h) : G = H := begin cases G with Gc G, cases H with Hc H, - apply (apd011 (Group.mk i) p), + apply (apd011 Group.mk p), exact group_pathover resp_mul end - definition Group_eq {i : signature} {G H : Group i} (f : carrier G ≃ carrier H) + definition Group_eq {G H : Group} (f : carrier G ≃ carrier H) (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H := Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹) diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 4dadf2dfc..638f96f16 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -14,10 +14,10 @@ open algebra pointed nat eq category group algebra is_trunc iso pointed unit tru namespace EM open groupoid_quotient - variables {i : signature} {G : Group i} - definition EM1 {i : signature} (G : Group i) : Type := + variables {G : Group} + definition EM1 (G : Group) : Type := groupoid_quotient (Groupoid_of_Group G) - definition pEM1 [constructor] {i : signature} (G : Group i) : Type* := + definition pEM1 [constructor] (G : Group) : Type* := pointed.MK (EM1 G) (elt star) definition base : EM1 G := elt star @@ -95,15 +95,15 @@ namespace EM end EM attribute EM.base [constructor] -attribute EM.rec EM.elim [unfold 8] [recursor 8] -attribute EM.rec_on EM.elim_on [unfold 5] -attribute EM.set_rec EM.set_elim [unfold 7] -attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 6] +attribute EM.rec EM.elim [unfold 7] [recursor 7] +attribute EM.rec_on EM.elim_on [unfold 4] +attribute EM.set_rec EM.set_elim [unfold 6] +attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5] namespace EM open groupoid_quotient - variables {i : signature} (G : Group i) + variables (G : Group) definition base_eq_base_equiv [constructor] : (base = base :> pEM1 G) ≃ G := !elt_eq_elt_equiv @@ -142,7 +142,7 @@ end EM open hopf susp namespace EM -- The K(G,n+1): - variables {i : signature} {G : CommGroup i} (n : ℕ) + variables {G : CommGroup} (n : ℕ) definition EM1_mul [unfold 2 3] (x x' : EM1 G) : EM1 G := begin @@ -211,7 +211,7 @@ namespace EM end /- K(G, n) -/ - definition EM {i : signature} (G : CommGroup i) : ℕ → Type* + definition EM (G : CommGroup) : ℕ → Type* | 0 := pType_of_Group G | (k+1) := EMadd1 G k @@ -248,7 +248,7 @@ namespace EM end /- Uniqueness of K(G, 1) -/ - variable {H : Group i} + variable {H : Group} definition pEM1_pmap [constructor] {X : Type*} (e : Ω X ≃ H) (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 H →* X := begin @@ -270,7 +270,7 @@ namespace EM end open trunc_index - definition pEM1_pequiv'.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : Ω X ≃ G) + definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G) (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X := begin apply pequiv_of_pmap (pEM1_pmap e r), @@ -287,7 +287,7 @@ namespace EM do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}} end - definition pEM1_pequiv.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : π₁ X ≃g G) + definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X := begin apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e), @@ -297,7 +297,7 @@ namespace EM definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X := pEM1_pequiv !isomorphism.refl - definition EM_pequiv_1.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} (e : π₁ X ≃g G) + definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X := begin refine _ ⬝e* pEM1_pequiv e, @@ -309,7 +309,7 @@ namespace EM definition EMadd1_pequiv_pEM1 : EMadd1 G 0 ≃* pEM1 G := begin apply ptrunc_pequiv, apply is_trunc_pEM1 end - definition EM1add1_pequiv_0.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} + definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X := EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index 39b935098..001855606 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -723,12 +723,12 @@ namespace chain_complex | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end - definition Group_LES_of_homotopy_groups (x : +3ℕ) : MulGroup.{u} := - MulGroup.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) + definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := + Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) (group_LES_of_homotopy_groups (pr1 x) (pr2 x)) - definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : MulCommGroup.{u} := - MulCommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) + definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} := + CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),