Define representations of monoids (#765)

src/category-theory.lagda.md

@@ -38,6 +38,8 @@ 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-in-precategories public
+open import category-theory.dependent-products-of-categories public
+open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
 open import category-theory.endomorphisms-in-categories public
 open import category-theory.endomorphisms-in-precategories public
@@ -46,6 +48,8 @@ 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.function-categories public
+open import category-theory.function-precategories public
 open import category-theory.functors-categories public
 open import category-theory.functors-large-precategories public
 open import category-theory.functors-precategories public
@@ -65,6 +69,7 @@ open import category-theory.natural-numbers-object-precategories public
 open import category-theory.natural-transformations-categories public
 open import category-theory.natural-transformations-large-precategories public
 open import category-theory.natural-transformations-precategories public
+open import category-theory.one-object-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.precategories public
 open import category-theory.precategory-of-functors public

src/category-theory/categories.lagda.md

@@ -86,6 +86,11 @@ module _
   associative-comp-hom-Category =
     associative-comp-hom-Precategory precategory-Category
 
+  associative-composition-structure-Category :
+    associative-composition-structure-Set hom-Category
+  associative-composition-structure-Category =
+    associative-composition-structure-Precategory precategory-Category
+
   id-hom-Category : {x : obj-Category} → type-hom-Category x x
   id-hom-Category = id-hom-Precategory precategory-Category
 
@@ -101,6 +106,13 @@ module _
   right-unit-law-comp-hom-Category =
     right-unit-law-comp-hom-Precategory precategory-Category
 
+  is-unital-composition-structure-Category :
+    is-unital-composition-structure-Set
+      hom-Category
+      associative-composition-structure-Category
+  is-unital-composition-structure-Category =
+    is-unital-composition-structure-Precategory precategory-Category
+
   is-category-Category :
     is-category-Precategory precategory-Category
   is-category-Category = pr2 C

src/category-theory/dependent-products-of-categories.lagda.md

@@ -0,0 +1,203 @@
+# Dependent products of categories
+
+```agda
+module category-theory.dependent-products-of-categories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.categories
+open import category-theory.dependent-products-of-precategories
+open import category-theory.isomorphisms-in-categories
+open import category-theory.precategories
+
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Given a family of [categories](category-theory.categories.md) `Cᵢ` indexed by
+`i : I`, the dependent product type `Π(i : I), Cᵢ` is a category consisting of
+functions taking `i : I` to an object of `Cᵢ`. Every component of the structure
+is given pointwise.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level} (I : UU l1) (C : I → Category l2 l3)
+  where
+
+  precategory-Π-Category : Precategory (l1 ⊔ l2) (l1 ⊔ l3)
+  precategory-Π-Category = Π-Precategory I (precategory-Category ∘ C)
+
+  abstract
+    is-category-precategory-Π-Category :
+      is-category-Precategory precategory-Π-Category
+    is-category-precategory-Π-Category x y =
+      is-equiv-htpy-equiv
+        ( equiv-iso-Π-fiberwise-iso-Precategory I (precategory-Category ∘ C) ∘e
+          equiv-Π-equiv-family
+            ( λ i → extensionality-obj-Category (C i) (x i) (y i)) ∘e
+          equiv-funext)
+        ( λ {refl → refl})
+
+  Π-Category : Category (l1 ⊔ l2) (l1 ⊔ l3)
+  pr1 Π-Category = Π-Precategory I (precategory-Category ∘ C)
+  pr2 Π-Category = is-category-precategory-Π-Category
+
+  obj-Π-Category : UU (l1 ⊔ l2)
+  obj-Π-Category = obj-Category Π-Category
+
+  hom-Π-Category :
+    obj-Π-Category → obj-Π-Category → Set (l1 ⊔ l3)
+  hom-Π-Category = hom-Category Π-Category
+
+  type-hom-Π-Category :
+    obj-Π-Category → obj-Π-Category → UU (l1 ⊔ l3)
+  type-hom-Π-Category = type-hom-Category Π-Category
+
+  comp-hom-Π-Category :
+    {x y z : obj-Π-Category} →
+    type-hom-Π-Category y z →
+    type-hom-Π-Category x y →
+    type-hom-Π-Category x z
+  comp-hom-Π-Category = comp-hom-Category Π-Category
+
+  associative-comp-hom-Π-Category :
+    {x y z w : obj-Π-Category}
+    (h : type-hom-Π-Category z w)
+    (g : type-hom-Π-Category y z)
+    (f : type-hom-Π-Category x y) →
+    ( comp-hom-Π-Category (comp-hom-Π-Category h g) f) ＝
+    ( comp-hom-Π-Category h (comp-hom-Π-Category g f))
+  associative-comp-hom-Π-Category =
+    associative-comp-hom-Category Π-Category
+
+  associative-composition-structure-Π-Category :
+    associative-composition-structure-Set hom-Π-Category
+  associative-composition-structure-Π-Category =
+    associative-composition-structure-Category Π-Category
+
+  id-hom-Π-Category :
+    {x : obj-Π-Category} → type-hom-Π-Category x x
+  id-hom-Π-Category = id-hom-Category Π-Category
+
+  left-unit-law-comp-hom-Π-Category :
+    {x y : obj-Π-Category}
+    (f : type-hom-Π-Category x y) →
+    comp-hom-Π-Category id-hom-Π-Category f ＝ f
+  left-unit-law-comp-hom-Π-Category =
+    left-unit-law-comp-hom-Category Π-Category
+
+  right-unit-law-comp-hom-Π-Category :
+    {x y : obj-Π-Category} (f : type-hom-Π-Category x y) →
+    comp-hom-Π-Category f id-hom-Π-Category ＝ f
+  right-unit-law-comp-hom-Π-Category =
+    right-unit-law-comp-hom-Category Π-Category
+
+  is-unital-Π-Category :
+    is-unital-composition-structure-Set
+      hom-Π-Category
+      associative-composition-structure-Π-Category
+  is-unital-Π-Category = is-unital-composition-structure-Category Π-Category
+
+  extensionality-obj-Π-Category :
+    (x y : obj-Category Π-Category) → (x ＝ y) ≃ iso-Category Π-Category x y
+  extensionality-obj-Π-Category = extensionality-obj-Category Π-Category
+```
+
+## Properties
+
+### Isomorphisms in the dependent product category are fiberwise isomorphisms
+
+```agda
+module _
+  {l1 l2 l3 : Level} (I : UU l1) (C : I → Category l2 l3)
+  {x y : obj-Π-Category I C}
+  where
+
+  is-fiberwise-iso-is-iso-Π-Category :
+    (f : type-hom-Π-Category I C x y) →
+    is-iso-Category (Π-Category I C) f →
+    (i : I) → is-iso-Category (C i) (f i)
+  is-fiberwise-iso-is-iso-Π-Category =
+    is-fiberwise-iso-is-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  fiberwise-iso-iso-Π-Category :
+    iso-Category (Π-Category I C) x y →
+    (i : I) → iso-Category (C i) (x i) (y i)
+  fiberwise-iso-iso-Π-Category =
+    fiberwise-iso-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  is-iso-Π-is-fiberwise-iso-Category :
+    (f : type-hom-Π-Category I C x y) →
+    ((i : I) → is-iso-Category (C i) (f i)) →
+    is-iso-Category (Π-Category I C) f
+  is-iso-Π-is-fiberwise-iso-Category =
+    is-iso-Π-is-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+
+  iso-Π-fiberwise-iso-Category :
+    ((i : I) → iso-Category (C i) (x i) (y i)) →
+    iso-Category (Π-Category I C) x y
+  iso-Π-fiberwise-iso-Category =
+    iso-Π-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+
+  is-equiv-is-fiberwise-iso-is-iso-Π-Category :
+    (f : type-hom-Π-Category I C x y) →
+    is-equiv (is-fiberwise-iso-is-iso-Π-Category f)
+  is-equiv-is-fiberwise-iso-is-iso-Π-Category =
+    is-equiv-is-fiberwise-iso-is-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  equiv-is-fiberwise-iso-is-iso-Π-Category :
+    (f : type-hom-Π-Category I C x y) →
+    ( is-iso-Category (Π-Category I C) f) ≃
+    ( (i : I) → is-iso-Category (C i) (f i))
+  equiv-is-fiberwise-iso-is-iso-Π-Category =
+    equiv-is-fiberwise-iso-is-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  is-equiv-is-iso-Π-is-fiberwise-iso-Category :
+    (f : type-hom-Π-Category I C x y) →
+    is-equiv (is-iso-Π-is-fiberwise-iso-Category f)
+  is-equiv-is-iso-Π-is-fiberwise-iso-Category =
+    is-equiv-is-iso-Π-is-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+
+  equiv-is-iso-Π-is-fiberwise-iso-Category :
+    ( f : type-hom-Π-Category I C x y) →
+    ( (i : I) → is-iso-Category (C i) (f i)) ≃
+    ( is-iso-Category (Π-Category I C) f)
+  equiv-is-iso-Π-is-fiberwise-iso-Category =
+    equiv-is-iso-Π-is-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+
+  is-equiv-fiberwise-iso-iso-Π-Category :
+    is-equiv fiberwise-iso-iso-Π-Category
+  is-equiv-fiberwise-iso-iso-Π-Category =
+    is-equiv-fiberwise-iso-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  equiv-fiberwise-iso-iso-Π-Category :
+    ( iso-Category (Π-Category I C) x y) ≃
+    ( (i : I) → iso-Category (C i) (x i) (y i))
+  equiv-fiberwise-iso-iso-Π-Category =
+    equiv-fiberwise-iso-iso-Π-Precategory I (precategory-Category ∘ C)
+
+  is-equiv-iso-Π-fiberwise-iso-Category :
+    is-equiv iso-Π-fiberwise-iso-Category
+  is-equiv-iso-Π-fiberwise-iso-Category =
+    is-equiv-iso-Π-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+
+  equiv-iso-Π-fiberwise-iso-Category :
+    ( (i : I) → iso-Category (C i) (x i) (y i)) ≃
+    ( iso-Category (Π-Category I C) x y)
+  equiv-iso-Π-fiberwise-iso-Category =
+    equiv-iso-Π-fiberwise-iso-Precategory I (precategory-Category ∘ C)
+```