Cleaning up for homotopy groups

src/foundation/connected-components.lagda.md

@@ -45,9 +45,9 @@ module _
   pr1 point-connected-component = a
   pr2 point-connected-component = unit-trunc-Prop refl
 
-  connected-component-Pointed-Type : Pointed-Type l
-  pr1 connected-component-Pointed-Type = connected-component
-  pr2 connected-component-Pointed-Type = point-connected-component
+  connected-component-pointed-type : Pointed-Type l
+  pr1 connected-component-pointed-type = connected-component
+  pr2 connected-component-pointed-type = point-connected-component
 
   value-connected-component :
     connected-component → A
@@ -71,11 +71,11 @@ abstract
     is-0-connected (connected-component A a)
   is-0-connected-connected-component A a =
     is-0-connected-mere-eq
-      ( pair a (unit-trunc-Prop refl))
-      ( λ (pair x p) →
+      ( a , unit-trunc-Prop refl)
+      ( λ (x , p) →
         apply-universal-property-trunc-Prop
           ( p)
-          ( trunc-Prop (pair a (unit-trunc-Prop refl) ＝ pair x p))
+          ( trunc-Prop ((a , unit-trunc-Prop refl) ＝ (x , p)))
           ( λ p' →
             unit-trunc-Prop
               ( eq-pair-Σ
@@ -84,7 +84,7 @@ abstract
 
 connected-component-∞-Group :
   {l : Level} (A : UU l) (a : A) → ∞-Group l
-pr1 (connected-component-∞-Group A a) = connected-component-Pointed-Type A a
+pr1 (connected-component-∞-Group A a) = connected-component-pointed-type A a
 pr2 (connected-component-∞-Group A a) = is-0-connected-connected-component A a
 ```
 

src/foundation/connected-types.lagda.md

@@ -31,16 +31,38 @@ A type is said to be **`k`-connected** if its `k`-truncation is contractible.
 
 ## Definition
 
+### The predicate of being a `k`-connected type
+
 ```agda
-is-connected-Prop : {l : Level} (k : 𝕋) → UU l → Prop l
-is-connected-Prop k A = is-contr-Prop (type-trunc k A)
+module _
+  {l : Level} (k : 𝕋) (A : UU l)
+  where
+
+  is-connected-Prop : Prop l
+  is-connected-Prop = is-contr-Prop (type-trunc k A)
+
+  is-connected : UU l
+  is-connected = type-Prop is-connected-Prop
+
+  is-prop-is-connected : is-prop is-connected
+  is-prop-is-connected = is-prop-type-Prop is-connected-Prop
+```
+
+### The type of `k`-connected types
+
+```agda
+Connected-Type : (l : Level) (k : 𝕋) → UU (lsuc l)
+Connected-Type l k = Σ (UU l) (is-connected k)
+
+module _
+  {l : Level} {k : 𝕋} (A : Connected-Type l k)
+  where
 
-is-connected : {l : Level} (k : 𝕋) → UU l → UU l
-is-connected k A = type-Prop (is-connected-Prop k A)
+  type-Connected-Type : UU l
+  type-Connected-Type = pr1 A
 
-is-prop-is-connected :
-  {l : Level} (k : 𝕋) (A : UU l) → is-prop (is-connected k A)
-is-prop-is-connected k A = is-prop-type-Prop (is-connected-Prop k A)
+  is-connected-Connected-Type : is-connected k type-Connected-Type
+  is-connected-Connected-Type = pr2 A
 ```
 
 ## Properties
@@ -50,8 +72,7 @@ is-prop-is-connected k A = is-prop-type-Prop (is-connected-Prop k A)
 ```agda
 is-equiv-diagonal-is-connected :
   {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k) →
-  is-connected k A →
-  is-equiv (λ (b : type-Truncated-Type B) → const A (type-Truncated-Type B) b)
+  is-connected k A → is-equiv (const A (type-Truncated-Type B))
 is-equiv-diagonal-is-connected B H =
   is-equiv-comp
     ( precomp unit-trunc (type-Truncated-Type B))

src/foundation/iterating-functions.lagda.md

@@ -161,3 +161,7 @@ module _
     eq-htpy (λ f → eq-htpy (λ x → iterate-mul-ℕ k l f x))
   pr2 (pr2 iterative-Monoid-Action) = refl
 ```
+
+## External links
+
+- [Function iteration](https://www.wikidata.org/wiki/Q5254619) on Wikidata

src/group-theory/automorphism-groups.lagda.md

@@ -7,7 +7,6 @@ module group-theory.automorphism-groups where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.0-connected-types
 open import foundation.1-types
 open import foundation.connected-components
 open import foundation.contractible-types
@@ -16,57 +15,23 @@ open import foundation.equivalences
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.identity-types
 open import foundation.propositional-truncations
-open import foundation.subtype-identity-principle
 open import foundation.universe-levels
 
 open import group-theory.concrete-groups
 open import group-theory.equivalences-concrete-groups
 
-open import higher-group-theory.equivalences-higher-groups
+open import higher-group-theory.automorphism-groups
 open import higher-group-theory.higher-groups
-
-open import structured-types.pointed-types
 ```
 
 </details>
 
 ## Idea
 
-The automorphim group of `a : A` is the group of symmetries of `a` in `A`.
+The **concrete automorphism group** of an element `a` of a [1-type](foundation.1-types.md) `A` is the [connected component](foundation.connected-components.md) of `a`.
 
 ## Definitions
 
-### Automorphism ∞-groups of a type
-
-```agda
-module _
-  {l : Level} (A : UU l) (a : A)
-  where
-
-  classifying-type-Automorphism-∞-Group : UU l
-  classifying-type-Automorphism-∞-Group = connected-component A a
-
-  shape-Automorphism-∞-Group : classifying-type-Automorphism-∞-Group
-  pr1 shape-Automorphism-∞-Group = a
-  pr2 shape-Automorphism-∞-Group = unit-trunc-Prop refl
-
-  classifying-pointed-type-Automorphism-∞-Group : Pointed-Type l
-  pr1 classifying-pointed-type-Automorphism-∞-Group =
-    classifying-type-Automorphism-∞-Group
-  pr2 classifying-pointed-type-Automorphism-∞-Group =
-    shape-Automorphism-∞-Group
-
-  is-0-connected-classifying-type-Automorphism-∞-Group :
-    is-0-connected classifying-type-Automorphism-∞-Group
-  is-0-connected-classifying-type-Automorphism-∞-Group =
-    is-0-connected-connected-component A a
-
-  Automorphism-∞-Group : ∞-Group l
-  pr1 Automorphism-∞-Group = classifying-pointed-type-Automorphism-∞-Group
-  pr2 Automorphism-∞-Group =
-    is-0-connected-classifying-type-Automorphism-∞-Group
-```
-
 ### Automorphism groups of objects in a 1-type
 
 ```agda
@@ -76,13 +41,13 @@ module _
 
   classifying-type-Automorphism-Group : UU l
   classifying-type-Automorphism-Group =
-    classifying-type-Automorphism-∞-Group (type-1-Type A) a
+    classifying-type-Automorphism-∞-Group a
 
   shape-Automorphism-Group : classifying-type-Automorphism-Group
-  shape-Automorphism-Group = shape-Automorphism-∞-Group (type-1-Type A) a
+  shape-Automorphism-Group = shape-Automorphism-∞-Group a
 
   Automorphism-Group : Concrete-Group l
-  pr1 Automorphism-Group = Automorphism-∞-Group (type-1-Type A) a
+  pr1 Automorphism-Group = Automorphism-∞-Group a
   pr2 Automorphism-Group =
     is-trunc-connected-component
       ( type-1-Type A)
@@ -97,64 +62,6 @@ module _
 
 ## Properties
 
-### Characerizing the identity type of `Automorphism-∞-Group`
-
-```agda
-module _
-  {l : Level} {A : UU l} (a : A)
-  where
-
-  Eq-classifying-type-Automorphism-∞-Group :
-    (X Y : classifying-type-Automorphism-∞-Group A a) → UU l
-  Eq-classifying-type-Automorphism-∞-Group X Y = pr1 X ＝ pr1 Y
-
-  refl-Eq-classifying-type-Automorphism-∞-Group :
-    (X : classifying-type-Automorphism-∞-Group A a) →
-    Eq-classifying-type-Automorphism-∞-Group X X
-  refl-Eq-classifying-type-Automorphism-∞-Group X = refl
-
-  is-contr-total-Eq-classifying-type-Automorphism-∞-Group :
-    (X : classifying-type-Automorphism-∞-Group A a) →
-    is-contr
-      ( Σ ( classifying-type-Automorphism-∞-Group A a)
-          ( Eq-classifying-type-Automorphism-∞-Group X))
-  is-contr-total-Eq-classifying-type-Automorphism-∞-Group X =
-    is-contr-total-Eq-subtype
-      ( is-contr-total-path (pr1 X))
-      ( λ a → is-prop-type-trunc-Prop)
-      ( pr1 X)
-      ( refl)
-      ( pr2 X)
-
-  Eq-eq-classifying-type-Automorphism-∞-Group :
-    (X Y : classifying-type-Automorphism-∞-Group A a) →
-    (X ＝ Y) → Eq-classifying-type-Automorphism-∞-Group X Y
-  Eq-eq-classifying-type-Automorphism-∞-Group X .X refl =
-    refl-Eq-classifying-type-Automorphism-∞-Group X
-
-  is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group :
-    (X Y : classifying-type-Automorphism-∞-Group A a) →
-    is-equiv (Eq-eq-classifying-type-Automorphism-∞-Group X Y)
-  is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group X =
-    fundamental-theorem-id
-      ( is-contr-total-Eq-classifying-type-Automorphism-∞-Group X)
-      ( Eq-eq-classifying-type-Automorphism-∞-Group X)
-
-  extensionality-classifying-type-Automorphism-∞-Group :
-    (X Y : classifying-type-Automorphism-∞-Group A a) →
-    (X ＝ Y) ≃ Eq-classifying-type-Automorphism-∞-Group X Y
-  pr1 (extensionality-classifying-type-Automorphism-∞-Group X Y) =
-    Eq-eq-classifying-type-Automorphism-∞-Group X Y
-  pr2 (extensionality-classifying-type-Automorphism-∞-Group X Y) =
-    is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group X Y
-
-  eq-Eq-classifying-type-Automorphism-∞-Group :
-    (X Y : classifying-type-Automorphism-∞-Group A a) →
-    Eq-classifying-type-Automorphism-∞-Group X Y → X ＝ Y
-  eq-Eq-classifying-type-Automorphism-∞-Group X Y =
-    map-inv-equiv (extensionality-classifying-type-Automorphism-∞-Group X Y)
-```
-
 ### Characerizing the identity type of `Automorphism-Group`
 
 ```agda
@@ -210,20 +117,6 @@ module _
     map-inv-equiv (extensionality-classifying-type-Automorphism-Group X Y)
 ```
 
-### Equal elements have equivalent automorphism ∞-groups
-
-```agda
-module _
-  {l : Level} {A : UU l}
-  where
-
-  equiv-eq-Automorphism-∞-Group :
-    {x y : A} (p : x ＝ y) →
-    equiv-∞-Group (Automorphism-∞-Group A x) (Automorphism-∞-Group A y)
-  equiv-eq-Automorphism-∞-Group refl =
-    id-equiv-∞-Group (Automorphism-∞-Group A _)
-```
-
 ### Equal elements in a 1-type have isomorphic automorphism groups
 
 ```agda

src/group-theory/concrete-groups.lagda.md

@@ -20,6 +20,8 @@ open import foundation.truncation-levels
 open import foundation.universe-levels
 
 open import group-theory.groups
+open import group-theory.monoids
+open import group-theory.semigroups
 
 open import higher-group-theory.higher-groups
 
@@ -157,21 +159,34 @@ module _
   right-inverse-law-mul-Concrete-Group =
     right-inverse-law-mul-∞-Group ∞-group-Concrete-Group
 
+  has-associative-mul-Concrete-Group :
+    has-associative-mul-Set set-Concrete-Group
+  pr1 has-associative-mul-Concrete-Group = mul-Concrete-Group
+  pr2 has-associative-mul-Concrete-Group = associative-mul-Concrete-Group
+
+  semigroup-Concrete-Group : Semigroup l
+  pr1 semigroup-Concrete-Group = set-Concrete-Group
+  pr2 semigroup-Concrete-Group = has-associative-mul-Concrete-Group
+
+  is-unital-Concrete-Group : is-unital-Semigroup semigroup-Concrete-Group
+  pr1 is-unital-Concrete-Group = unit-Concrete-Group
+  pr1 (pr2 is-unital-Concrete-Group) = left-unit-law-mul-Concrete-Group
+  pr2 (pr2 is-unital-Concrete-Group) = right-unit-law-mul-Concrete-Group
+
+  monoid-Concrete-Group : Monoid l
+  pr1 monoid-Concrete-Group = semigroup-Concrete-Group
+  pr2 monoid-Concrete-Group = is-unital-Concrete-Group
+
+  is-group-Concrete-Group :
+    is-group semigroup-Concrete-Group
+  pr1 is-group-Concrete-Group = is-unital-Concrete-Group
+  pr1 (pr2 is-group-Concrete-Group) = inv-Concrete-Group
+  pr1 (pr2 (pr2 is-group-Concrete-Group)) = left-inverse-law-mul-Concrete-Group
+  pr2 (pr2 (pr2 is-group-Concrete-Group)) = right-inverse-law-mul-Concrete-Group
+
   abstract-group-Concrete-Group : Group l
-  pr1 (pr1 abstract-group-Concrete-Group) = set-Concrete-Group
-  pr1 (pr2 (pr1 abstract-group-Concrete-Group)) = mul-Concrete-Group
-  pr2 (pr2 (pr1 abstract-group-Concrete-Group)) = associative-mul-Concrete-Group
-  pr1 (pr1 (pr2 abstract-group-Concrete-Group)) = unit-Concrete-Group
-  pr1 (pr2 (pr1 (pr2 abstract-group-Concrete-Group))) =
-    left-unit-law-mul-Concrete-Group
-  pr2 (pr2 (pr1 (pr2 abstract-group-Concrete-Group))) =
-    right-unit-law-mul-Concrete-Group
-  pr1 (pr2 (pr2 abstract-group-Concrete-Group)) =
-    inv-Concrete-Group
-  pr1 (pr2 (pr2 (pr2 abstract-group-Concrete-Group))) =
-    left-inverse-law-mul-Concrete-Group
-  pr2 (pr2 (pr2 (pr2 abstract-group-Concrete-Group))) =
-    right-inverse-law-mul-Concrete-Group
+  pr1 abstract-group-Concrete-Group = semigroup-Concrete-Group
+  pr2 abstract-group-Concrete-Group = is-group-Concrete-Group
 
   op-abstract-group-Concrete-Group : Group l
   pr1 (pr1 op-abstract-group-Concrete-Group) = set-Concrete-Group

src/higher-group-theory.lagda.md

@@ -5,6 +5,7 @@
 ```agda
 module higher-group-theory where
 
+open import higher-group-theory.automorphism-groups public
 open import higher-group-theory.cartesian-products-higher-groups public
 open import higher-group-theory.conjugation public
 open import higher-group-theory.cyclic-higher-groups public