Refactor structured monoids (#761)

Co-authored-by: Egbert Rijke <[email protected]>

src/category-theory.lagda.md

@@ -34,28 +34,30 @@
 module category-theory where
 
 open import category-theory.adjunctions-large-precategories public
-open import category-theory.anafunctors public
+open import category-theory.anafunctors-categories public
+open import category-theory.anafunctors-precategories public
 open import category-theory.categories public
-open import category-theory.coproducts-precategories public
+open import category-theory.coproducts-in-precategories public
 open import category-theory.discrete-categories public
-open import category-theory.endomorphisms-of-objects-categories public
-open import category-theory.epimorphisms-large-precategories public
-open import category-theory.equivalences-categories public
-open import category-theory.equivalences-large-precategories public
-open import category-theory.equivalences-precategories public
-open import category-theory.exponential-objects-precategories public
+open import category-theory.endomorphisms-in-categories public
+open import category-theory.endomorphisms-in-precategories public
+open import category-theory.epimorphisms-in-large-precategories public
+open import category-theory.equivalences-of-categories public
+open import category-theory.equivalences-of-large-precategories public
+open import category-theory.equivalences-of-precategories public
+open import category-theory.exponential-objects-in-precategories public
 open import category-theory.functors-categories public
 open import category-theory.functors-large-precategories public
 open import category-theory.functors-precategories public
 open import category-theory.groupoids public
 open import category-theory.homotopies-natural-transformations-large-precategories public
-open import category-theory.initial-objects-precategories public
-open import category-theory.isomorphisms-categories public
-open import category-theory.isomorphisms-large-precategories public
-open import category-theory.isomorphisms-precategories public
+open import category-theory.initial-objects-in-precategories public
+open import category-theory.isomorphisms-in-categories public
+open import category-theory.isomorphisms-in-large-precategories public
+open import category-theory.isomorphisms-in-precategories public
 open import category-theory.large-categories public
 open import category-theory.large-precategories public
-open import category-theory.monomorphisms-large-precategories public
+open import category-theory.monomorphisms-in-large-precategories public
 open import category-theory.natural-isomorphisms-categories public
 open import category-theory.natural-isomorphisms-large-precategories public
 open import category-theory.natural-isomorphisms-precategories public
@@ -67,12 +69,12 @@ open import category-theory.opposite-precategories public
 open import category-theory.precategories public
 open import category-theory.precategory-of-functors public
 open import category-theory.pregroupoids public
+open import category-theory.products-in-precategories public
 open import category-theory.products-of-precategories public
-open import category-theory.products-precategories public
-open import category-theory.pullbacks-precategories public
+open import category-theory.pullbacks-in-precategories public
 open import category-theory.representable-functors-precategories public
-open import category-theory.sieves-categories public
+open import category-theory.sieves-in-categories public
 open import category-theory.slice-precategories public
-open import category-theory.terminal-objects-precategories public
+open import category-theory.terminal-objects-in-precategories public
 open import category-theory.yoneda-lemma-precategories public
 ```

src/category-theory/anafunctors-categories.lagda.md

@@ -0,0 +1,91 @@
+# Anafunctors between categories
+
+```agda
+module category-theory.anafunctors-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.anafunctors-precategories
+open import category-theory.categories
+open import category-theory.functors-categories
+open import category-theory.functors-precategories
+open import category-theory.isomorphisms-in-precategories
+open import category-theory.precategories
+
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An **anafunctor** is a [functor](category-theory.functors-categories.md) that is
+only defined up to [isomorphism](category-theory.isomorphisms-in-categories.md).
+
+## Definition
+
+```agda
+anafunctor-Category :
+  {l1 l2 l3 l4 : Level} (l : Level) →
+  Category l1 l2 → Category l3 l4 → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
+anafunctor-Category l C D =
+  anafunctor-Precategory l (precategory-Category C) (precategory-Category D)
+
+module _
+  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4)
+  (F : anafunctor-Category l5 C D)
+  where
+
+  object-anafunctor-Category : obj-Category C → obj-Category D → UU l5
+  object-anafunctor-Category =
+    object-anafunctor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+
+  hom-anafunctor-Category :
+    (X Y : obj-Category C) (U : obj-Category D)
+    (u : object-anafunctor-Category X U)
+    (V : obj-Category D) (v : object-anafunctor-Category Y V) →
+    type-hom-Category C X Y → type-hom-Category D U V
+  hom-anafunctor-Category =
+    hom-anafunctor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+      ( F)
+```
+
+## Properties
+
+### Any functor between categories induces an anafunctor
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Category l1 l2) (D : Category l3 l4)
+  where
+
+  anafunctor-functor-Category :
+    functor-Category C D → anafunctor-Category l4 C D
+  anafunctor-functor-Category =
+    anafunctor-functor-Precategory
+      ( precategory-Category C)
+      ( precategory-Category D)
+```
+
+### The action on objects of an anafunctor between categories
+
+```agda
+image-object-anafunctor-Category :
+  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4) →
+  anafunctor-Category l5 C D → obj-Category C → UU (l3 ⊔ l5)
+image-object-anafunctor-Category C D F X =
+  Σ ( obj-Category D)
+    ( λ U → type-trunc-Prop (object-anafunctor-Category C D F X U))
+```

src/category-theory/anafunctors.lagda.md → src/category-theory/anafunctors-precategories.lagda.md

@@ -1,15 +1,15 @@
-# Anafunctors
+# Anafunctors between precategories
 
 ```agda
-module category-theory.anafunctors where
+module category-theory.anafunctors-precategories where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
 open import category-theory.categories
 open import category-theory.functors-precategories
-open import category-theory.isomorphisms-precategories
+open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.action-on-identifications-functions
@@ -24,12 +24,12 @@ open import foundation.universe-levels
 
 ## Idea
 
-An anafunctor is a functor that is only defined up to isomorphism.
+An **anafunctor** is a [functor](category-theory.functors-precategories.md) that
+is only defined up to
+[isomorphism](category-theory.isomorphisms-in-precategories.md).
 
 ## Definition
 
-### Anafunctors between precategories
-
 ```agda
 anafunctor-Precategory :
   {l1 l2 l3 l4 : Level} (l : Level) →
@@ -74,39 +74,6 @@ module _
   hom-anafunctor-Precategory = pr1 (pr2 F)
 ```
 
-### Anafunctors between categories
-
-```agda
-anafunctor-Category :
-  {l1 l2 l3 l4 : Level} (l : Level) →
-  Category l1 l2 → Category l3 l4 → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
-anafunctor-Category l C D =
-  anafunctor-Precategory l (precategory-Category C) (precategory-Category D)
-
-module _
-  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4)
-  (F : anafunctor-Category l5 C D)
-  where
-
-  object-anafunctor-Category : obj-Category C → obj-Category D → UU l5
-  object-anafunctor-Category =
-    object-anafunctor-Precategory
-      ( precategory-Category C)
-      ( precategory-Category D)
-      ( F)
-
-  hom-anafunctor-Category :
-    (X Y : obj-Category C) (U : obj-Category D)
-    (u : object-anafunctor-Category X U)
-    (V : obj-Category D) (v : object-anafunctor-Category Y V) →
-    type-hom-Category C X Y → type-hom-Category D U V
-  hom-anafunctor-Category =
-    hom-anafunctor-Precategory
-      ( precategory-Category C)
-      ( precategory-Category D)
-      ( F)
-```
-
 ## Properties
 
 ### Any functor between precategories induces an anafunctor
@@ -188,14 +155,3 @@ module _
         ( hom-functor-Precategory C D F f))
       ( hom-inv-iso-Precategory D u))
 ```
-
-### The action on objects
-
-```agda
-image-object-anafunctor-Category :
-  {l1 l2 l3 l4 l5 : Level} (C : Category l1 l2) (D : Category l3 l4) →
-  anafunctor-Category l5 C D → obj-Category C → UU (l3 ⊔ l5)
-image-object-anafunctor-Category C D F X =
-  Σ ( obj-Category D)
-    ( λ U → type-trunc-Prop (object-anafunctor-Category C D F X U))
-```

src/category-theory/categories.lagda.md

@@ -7,7 +7,7 @@ module category-theory.categories where
 <details><summary>Imports</summary>
 
 ```agda
-open import category-theory.isomorphisms-precategories
+open import category-theory.isomorphisms-in-precategories
 open import category-theory.precategories
 
 open import foundation.1-types

src/category-theory/coproducts-precategories.lagda.md → src/category-theory/coproducts-in-precategories.lagda.md

@@ -1,7 +1,7 @@
 # Coproducts in precategories
 
 ```agda
-module category-theory.coproducts-precategories where
+module category-theory.coproducts-in-precategories where
 ```
 
 <details><summary>Imports</summary>

src/category-theory/endomorphisms-in-categories.lagda.md

@@ -0,0 +1,69 @@
+# Endomorphisms in categories
+
+```agda
+module category-theory.endomorphisms-in-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.endomorphisms-in-precategories
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import group-theory.monoids
+open import group-theory.semigroups
+```
+
+</details>
+
+## Definition
+
+### The monoid of endomorphisms on an object in a category
+
+```agda
+module _
+  {l1 l2 : Level} (C : Category l1 l2) (X : obj-Category C)
+  where
+
+  type-endo-Category : UU l2
+  type-endo-Category = type-endo-Precategory (precategory-Category C) X
+
+  comp-endo-Category :
+    type-endo-Category → type-endo-Category → type-endo-Category
+  comp-endo-Category = comp-endo-Precategory (precategory-Category C) X
+
+  id-endo-Category : type-endo-Category
+  id-endo-Category = id-endo-Precategory (precategory-Category C) X
+
+  associative-comp-endo-Category :
+    (h g f : type-endo-Category) →
+    ( comp-endo-Category (comp-endo-Category h g) f) ＝
+    ( comp-endo-Category h (comp-endo-Category g f))
+  associative-comp-endo-Category =
+    associative-comp-endo-Precategory (precategory-Category C) X
+
+  left-unit-law-comp-endo-Category :
+    (f : type-endo-Category) → comp-endo-Category id-endo-Category f ＝ f
+  left-unit-law-comp-endo-Category =
+    left-unit-law-comp-endo-Precategory (precategory-Category C) X
+
+  right-unit-law-comp-endo-Category :
+    (f : type-endo-Category) → comp-endo-Category f id-endo-Category ＝ f
+  right-unit-law-comp-endo-Category =
+    right-unit-law-comp-endo-Precategory (precategory-Category C) X
+
+  set-endo-Category : Set l2
+  set-endo-Category = set-endo-Precategory (precategory-Category C) X
+
+  semigroup-endo-Category : Semigroup l2
+  semigroup-endo-Category =
+    semigroup-endo-Precategory (precategory-Category C) X
+
+  monoid-endo-Category : Monoid l2
+  monoid-endo-Category = monoid-endo-Precategory (precategory-Category C) X
+```