refactoring pointed maps (#682)

Since pointed maps use all the information of pointed types, the domain
and codomain of a pointed map can be implicit.

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

@@ -159,13 +159,8 @@ module _
     is-connected-classifying-type-subgroup-Concrete-Group
   pr2 concrete-group-subgroup-Concrete-Group =
     is-set-is-emb
-      ( map-Ω
-        ( classifying-pointed-type-subgroup-Concrete-Group)
-        ( classifying-pointed-type-Concrete-Group G)
-        ( classifying-pointed-inclusion-subgroup-Concrete-Group))
+      ( map-Ω (classifying-pointed-inclusion-subgroup-Concrete-Group))
       ( is-emb-map-Ω
-        ( classifying-pointed-type-subgroup-Concrete-Group)
-        ( classifying-pointed-type-Concrete-Group G)
         ( classifying-pointed-inclusion-subgroup-Concrete-Group)
         ( is-faithful-classifying-inclusion-subgroup-Concrete-Group))
       ( is-set-type-Concrete-Group G)

src/higher-group-theory.lagda.md

@@ -7,6 +7,7 @@ module higher-group-theory where
 
 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
 open import higher-group-theory.equivalences-higher-groups public
 open import higher-group-theory.fixed-points-higher-group-actions public
 open import higher-group-theory.free-higher-group-actions public

src/higher-group-theory/conjugation.lagda.md

@@ -56,6 +56,5 @@ module _
     map-conjugation-Ω g ~ map-conjugation-∞-Group
   compute-map-conjugation-∞-Group =
     htpy-compute-action-on-loops-conjugation-Pointed-Type
-      ( classifying-pointed-type-∞-Group G)
       ( g)
 ```

src/higher-group-theory/cyclic-higher-groups.lagda.md

@@ -0,0 +1,58 @@
+# Cyclic higher groups
+
+```agda
+module higher-group-theory.cyclic-higher-groups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.embeddings
+open import foundation.existential-quantification
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import structured-types.pointed-maps
+open import structured-types.pointed-types
+
+open import synthetic-homotopy-theory.functoriality-loop-spaces
+open import synthetic-homotopy-theory.loop-spaces
+```
+
+</details>
+
+## Idea
+
+A [pointed type](structured-types.pointed-types.md) `A` is said to be cyclic if
+there [exists](foundation.existential-quantification.md) a
+[loop](synthetic-homotopy-theory.loop-spaces.md) `ω : Ω A` such that the
+evaluation map
+
+```text
+  (A →∗ B) → Ω B
+```
+
+given by `f ↦ Ω f ω` is an [embedding](foundation.embeddings.md) for every
+pointed type `B`. In other words, a pointed type is cyclic if its loop space is
+generated by a single element.
+
+## Definitions
+
+```agda
+ev-loop-Pointed-Type :
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (ω : type-Ω A) →
+  (A →∗ B) → type-Ω B
+ev-loop-Pointed-Type ω f = map-Ω f ω
+
+module _
+  {l1 : Level} (A : Pointed-Type l1)
+  where
+
+  is-cyclic-prop-Pointed-Type : (l2 : Level) → Prop (l1 ⊔ lsuc l2)
+  is-cyclic-prop-Pointed-Type l2 =
+    ∃-Prop
+      ( type-Ω A)
+      ( λ ω →
+        (B : Pointed-Type l2) →
+        is-emb (ev-loop-Pointed-Type {l1} {l2} {A} {B} ω))
+```

src/higher-group-theory/equivalences-higher-groups.lagda.md

@@ -42,8 +42,6 @@ module _
   hom-equiv-∞-Group : equiv-∞-Group → hom-∞-Group G H
   hom-equiv-∞-Group =
     pointed-map-pointed-equiv
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
 
   map-equiv-∞-Group : equiv-∞-Group → type-∞-Group G → type-∞-Group H
   map-equiv-∞-Group = map-hom-∞-Group G H ∘ hom-equiv-∞-Group
@@ -54,7 +52,7 @@ module _
 ```agda
 id-equiv-∞-Group :
   {l1 : Level} (G : ∞-Group l1) → equiv-∞-Group G G
-id-equiv-∞-Group G = id-pointed-equiv (classifying-pointed-type-∞-Group G)
+id-equiv-∞-Group G = id-pointed-equiv
 ```
 
 ### Isomorphisms of ∞-groups
@@ -65,10 +63,7 @@ module _
   where
 
   is-iso-hom-∞-Group : hom-∞-Group G H → UU (l1 ⊔ l2)
-  is-iso-hom-∞-Group =
-    is-iso-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+  is-iso-hom-∞-Group = is-iso-pointed-map
 ```
 
 ## Properties
@@ -83,7 +78,7 @@ is-contr-total-equiv-∞-Group G =
     ( is-contr-total-equiv-Pointed-Type (classifying-pointed-type-∞-Group G))
     ( λ X → is-prop-is-0-connected (type-Pointed-Type X))
     ( classifying-pointed-type-∞-Group G)
-    ( id-pointed-equiv (classifying-pointed-type-∞-Group G))
+    ( id-pointed-equiv)
     ( is-0-connected-classifying-type-∞-Group G)
 
 equiv-eq-∞-Group :

src/higher-group-theory/homomorphisms-higher-groups.lagda.md

@@ -38,51 +38,31 @@ module _
 
   classifying-map-hom-∞-Group :
     hom-∞-Group → classifying-type-∞-Group G → classifying-type-∞-Group H
-  classifying-map-hom-∞-Group =
-    map-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+  classifying-map-hom-∞-Group = map-pointed-map
 
   preserves-point-classifying-map-hom-∞-Group :
     (f : hom-∞-Group) →
-    Id (classifying-map-hom-∞-Group f (shape-∞-Group G)) (shape-∞-Group H)
+    classifying-map-hom-∞-Group f (shape-∞-Group G) ＝ shape-∞-Group H
   preserves-point-classifying-map-hom-∞-Group =
     preserves-point-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
 
   map-hom-∞-Group : hom-∞-Group → type-∞-Group G → type-∞-Group H
-  map-hom-∞-Group =
-    map-Ω
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+  map-hom-∞-Group = map-Ω
 
   preserves-unit-map-hom-∞-Group :
-    (f : hom-∞-Group) → Id (map-hom-∞-Group f (unit-∞-Group G)) (unit-∞-Group H)
-  preserves-unit-map-hom-∞-Group =
-    preserves-refl-map-Ω
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+    (f : hom-∞-Group) → map-hom-∞-Group f (unit-∞-Group G) ＝ unit-∞-Group H
+  preserves-unit-map-hom-∞-Group = preserves-refl-map-Ω
 
   preserves-mul-map-hom-∞-Group :
     (f : hom-∞-Group) (x y : type-∞-Group G) →
-    Id
-      ( map-hom-∞-Group f (mul-∞-Group G x y))
-      ( mul-∞-Group H (map-hom-∞-Group f x) (map-hom-∞-Group f y))
-  preserves-mul-map-hom-∞-Group =
-    preserves-mul-map-Ω
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+    map-hom-∞-Group f (mul-∞-Group G x y) ＝
+    mul-∞-Group H (map-hom-∞-Group f x) (map-hom-∞-Group f y)
+  preserves-mul-map-hom-∞-Group = preserves-mul-map-Ω
 
   preserves-inv-map-hom-∞-Group :
     (f : hom-∞-Group) (x : type-∞-Group G) →
-    Id
-      ( map-hom-∞-Group f (inv-∞-Group G x))
-      ( inv-∞-Group H (map-hom-∞-Group f x))
-  preserves-inv-map-hom-∞-Group =
-    preserves-inv-map-Ω
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+    map-hom-∞-Group f (inv-∞-Group G x) ＝ inv-∞-Group H (map-hom-∞-Group f x)
+  preserves-inv-map-hom-∞-Group = preserves-inv-map-Ω
 ```
 
 ## Properties
@@ -94,24 +74,15 @@ module _
   {l1 l2 : Level} (G : ∞-Group l1) (H : ∞-Group l2) (f : hom-∞-Group G H)
   where
 
-  htpy-hom-∞-Group :
-    (g : hom-∞-Group G H) → UU (l1 ⊔ l2)
-  htpy-hom-∞-Group =
-    htpy-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
-      ( f)
+  htpy-hom-∞-Group : (g : hom-∞-Group G H) → UU (l1 ⊔ l2)
+  htpy-hom-∞-Group = htpy-pointed-map f
 
   extensionality-hom-∞-Group :
-    (g : hom-∞-Group G H) → Id f g ≃ htpy-hom-∞-Group g
-  extensionality-hom-∞-Group =
-    extensionality-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
-      ( f)
+    (g : hom-∞-Group G H) → (f ＝ g) ≃ htpy-hom-∞-Group g
+  extensionality-hom-∞-Group = extensionality-pointed-map f
 
   eq-htpy-hom-∞-Group :
-    (g : hom-∞-Group G H) → (htpy-hom-∞-Group g) → Id f g
+    (g : hom-∞-Group G H) → (htpy-hom-∞-Group g) → f ＝ g
   eq-htpy-hom-∞-Group g = map-inv-equiv (extensionality-hom-∞-Group g)
 ```
 
@@ -131,11 +102,7 @@ module _
 
   comp-hom-∞-Group :
     hom-∞-Group H K → hom-∞-Group G H → hom-∞-Group G K
-  comp-hom-∞-Group =
-    comp-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
-      ( classifying-pointed-type-∞-Group K)
+  comp-hom-∞-Group = comp-pointed-map
 
 module _
   {l1 l2 l3 l4 : Level}
@@ -147,12 +114,7 @@ module _
     htpy-hom-∞-Group G L
       ( comp-hom-∞-Group G H L (comp-hom-∞-Group H K L h g) f)
       ( comp-hom-∞-Group G K L h (comp-hom-∞-Group G H K g f))
-  associative-comp-hom-∞-Group =
-    associative-comp-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
-      ( classifying-pointed-type-∞-Group K)
-      ( classifying-pointed-type-∞-Group L)
+  associative-comp-hom-∞-Group = associative-comp-pointed-map
 
 module _
   {l1 l2 : Level} (G : ∞-Group l1) (H : ∞-Group l2)
@@ -161,16 +123,10 @@ module _
   left-unit-law-comp-hom-∞-Group :
     (f : hom-∞-Group G H) →
     htpy-hom-∞-Group G H (comp-hom-∞-Group G H H (id-hom-∞-Group H) f) f
-  left-unit-law-comp-hom-∞-Group =
-    left-unit-law-comp-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+  left-unit-law-comp-hom-∞-Group = left-unit-law-comp-pointed-map
 
   right-unit-law-comp-hom-∞-Group :
     (f : hom-∞-Group G H) →
     htpy-hom-∞-Group G H (comp-hom-∞-Group G G H f (id-hom-∞-Group G)) f
-  right-unit-law-comp-hom-∞-Group =
-    right-unit-law-comp-pointed-map
-      ( classifying-pointed-type-∞-Group G)
-      ( classifying-pointed-type-∞-Group H)
+  right-unit-law-comp-hom-∞-Group = right-unit-law-comp-pointed-map
 ```

src/structured-types/conjugation-pointed-types.lagda.md

@@ -64,33 +64,27 @@ module _
 
 ```agda
 module _
-  {l : Level} (B : Pointed-Type l)
+  {l : Level} {B : Pointed-Type l}
   where
 
   action-on-loops-conjugation-Pointed-Type :
     {u : type-Pointed-Type B} (p : point-Pointed-Type B ＝ u) →
     Ω B →∗ Ω (type-Pointed-Type B , u)
   action-on-loops-conjugation-Pointed-Type p =
-    pointed-map-Ω B
-      ( type-Pointed-Type B , _)
-      ( conjugation-Pointed-Type B p)
+    pointed-map-Ω (conjugation-Pointed-Type B p)
 
   map-action-on-loops-conjugation-Pointed-Type :
     {u : type-Pointed-Type B} (p : point-Pointed-Type B ＝ u) →
     type-Ω B → type-Ω (type-Pointed-Type B , u)
   map-action-on-loops-conjugation-Pointed-Type p =
     map-pointed-map
-      ( Ω B)
-      ( Ω (type-Pointed-Type B , _))
       ( action-on-loops-conjugation-Pointed-Type p)
 
   preserves-point-action-on-loops-conjugation-Pointed-Type :
     {u : type-Pointed-Type B} (p : point-Pointed-Type B ＝ u) →
     map-action-on-loops-conjugation-Pointed-Type p refl ＝ refl
   preserves-point-action-on-loops-conjugation-Pointed-Type p =
     preserves-point-pointed-map
-      ( Ω B)
-      ( Ω (type-Pointed-Type B , _))
       ( action-on-loops-conjugation-Pointed-Type p)
 
   compute-action-on-loops-conjugation-Pointed-Type' :
@@ -104,8 +98,6 @@ module _
     conjugation-Ω p ~∗ action-on-loops-conjugation-Pointed-Type p
   compute-action-on-loops-conjugation-Pointed-Type p =
     concat-htpy-pointed-map
-      ( Ω B)
-      ( Ω (type-Pointed-Type B , _))
       ( conjugation-Ω p) (conjugation-Ω' p)
       ( action-on-loops-conjugation-Pointed-Type p)
       ( compute-conjugation-Ω p)

src/structured-types/faithful-pointed-maps.lagda.md

@@ -29,10 +29,10 @@ the underlying map is faithful.
 faithful-pointed-map :
   {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) → UU (l1 ⊔ l2)
 faithful-pointed-map A B =
-  Σ (A →∗ B) (λ f → is-faithful (map-pointed-map A B f))
+  Σ (A →∗ B) (λ f → is-faithful (map-pointed-map f))
 
 module _
-  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2)
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
   (f : faithful-pointed-map A B)
   where
 
@@ -41,12 +41,12 @@ module _
 
   map-faithful-pointed-map : type-Pointed-Type A → type-Pointed-Type B
   map-faithful-pointed-map =
-    map-pointed-map A B pointed-map-faithful-pointed-map
+    map-pointed-map pointed-map-faithful-pointed-map
 
   preserves-point-faithful-pointed-map :
     map-faithful-pointed-map (point-Pointed-Type A) ＝ point-Pointed-Type B
   preserves-point-faithful-pointed-map =
-    preserves-point-pointed-map A B pointed-map-faithful-pointed-map
+    preserves-point-pointed-map pointed-map-faithful-pointed-map
 
   is-faithful-faithful-pointed-map : is-faithful map-faithful-pointed-map
   is-faithful-faithful-pointed-map = pr2 f

src/structured-types/fibers-of-pointed-maps.lagda.md

@@ -21,10 +21,9 @@ open import structured-types.pointed-types
 
 ```agda
 fib-Pointed-Type :
-  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) →
+  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} →
   (A →∗ B) → Pointed-Type (l1 ⊔ l2)
-pr1 (fib-Pointed-Type A B f) =
-  fib (map-pointed-map A B f) (point-Pointed-Type B)
-pr1 (pr2 (fib-Pointed-Type A B f)) = point-Pointed-Type A
-pr2 (pr2 (fib-Pointed-Type A B f)) = preserves-point-pointed-map A B f
+pr1 (fib-Pointed-Type f) = fib (map-pointed-map f) (point-Pointed-Type _)
+pr1 (pr2 (fib-Pointed-Type f)) = point-Pointed-Type _
+pr2 (pr2 (fib-Pointed-Type f)) = preserves-point-pointed-map f
 ```