Merge branch 'master' into perfect-cores

src/category-theory.lagda.md

@@ -16,6 +16,7 @@ module category-theory where
 open import category-theory.adjunctions-large-precategories public
 open import category-theory.anafunctors-categories public
 open import category-theory.anafunctors-precategories public
+open import category-theory.augmented-simplex-category public
 open import category-theory.categories public
 open import category-theory.category-of-functors public
 open import category-theory.category-of-functors-from-small-to-large-categories public
@@ -29,6 +30,8 @@ open import category-theory.dependent-products-of-large-categories public
 open import category-theory.dependent-products-of-large-precategories public
 open import category-theory.dependent-products-of-precategories public
 open import category-theory.discrete-categories public
+open import category-theory.embedding-maps-precategories public
+open import category-theory.embeddings-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
@@ -37,6 +40,7 @@ open import category-theory.equivalences-of-large-precategories public
 open import category-theory.equivalences-of-precategories public
 open import category-theory.exponential-objects-precategories public
 open import category-theory.faithful-functors-precategories public
+open import category-theory.faithful-maps-precategories public
 open import category-theory.full-large-subcategories public
 open import category-theory.full-large-subprecategories public
 open import category-theory.function-categories public
@@ -96,6 +100,7 @@ open import category-theory.representable-functors-large-precategories public
 open import category-theory.representable-functors-precategories public
 open import category-theory.representing-arrow-category public
 open import category-theory.sieves-in-categories public
+open import category-theory.simplex-category public
 open import category-theory.slice-precategories public
 open import category-theory.subprecategories public
 open import category-theory.terminal-objects-precategories public

src/category-theory/augmented-simplex-category.lagda.md

@@ -0,0 +1,143 @@
+# The augmented simplex category
+
+```agda
+module category-theory.augmented-simplex-category where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.precategories
+
+open import elementary-number-theory.inequality-standard-finite-types
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import order-theory.order-preserving-maps-posets
+```
+
+</details>
+
+## Idea
+
+**The augmented simplex category** is the category consisting of
+[finite total orders](order-theory.finite-total-orders.md) and
+[order-preserving maps](order-theory.order-preserving-maps-posets.md). However,
+we define it as the category whose objects are
+[natural numbers](elementary-number-theory.natural-numbers.md) and whose
+hom-[sets](foundation-core.sets.md) `hom n m` are order-preserving maps between
+the [standard finite types](univalent-combinatorics.standard-finite-types.md)
+`Fin n` to `Fin m` [equipped](foundation.structure.md) with the
+[standard ordering](elementary-number-theory.inequality-standard-finite-types.md),
+and then show that it is
+[equivalent](category-theory.equivalences-of-precategories.md) to the former.
+
+## Definition
+
+### The augmented simplex precategory
+
+```agda
+obj-augmented-simplex-Category : UU lzero
+obj-augmented-simplex-Category = ℕ
+
+hom-set-augmented-simplex-Category :
+  obj-augmented-simplex-Category → obj-augmented-simplex-Category → Set lzero
+hom-set-augmented-simplex-Category n m =
+  hom-set-Poset (Fin-Poset n) (Fin-Poset m)
+
+hom-augmented-simplex-Category :
+  obj-augmented-simplex-Category → obj-augmented-simplex-Category → UU lzero
+hom-augmented-simplex-Category n m =
+  type-Set (hom-set-augmented-simplex-Category n m)
+
+comp-hom-augmented-simplex-Category :
+  {n m r : obj-augmented-simplex-Category} →
+  hom-augmented-simplex-Category m r →
+  hom-augmented-simplex-Category n m →
+  hom-augmented-simplex-Category n r
+comp-hom-augmented-simplex-Category {n} {m} {r} =
+  comp-hom-Poset (Fin-Poset n) (Fin-Poset m) (Fin-Poset r)
+
+associative-comp-hom-augmented-simplex-Category :
+  {n m r s : obj-augmented-simplex-Category}
+  (h : hom-augmented-simplex-Category r s)
+  (g : hom-augmented-simplex-Category m r)
+  (f : hom-augmented-simplex-Category n m) →
+  ( comp-hom-augmented-simplex-Category {n} {m} {s}
+    ( comp-hom-augmented-simplex-Category {m} {r} {s} h g)
+    ( f)) ＝
+  ( comp-hom-augmented-simplex-Category {n} {r} {s}
+    ( h)
+    ( comp-hom-augmented-simplex-Category {n} {m} {r} g f))
+associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-Poset
+    ( Fin-Poset n)
+    ( Fin-Poset m)
+    ( Fin-Poset r)
+    ( Fin-Poset s)
+
+associative-composition-structure-augmented-simplex-Category :
+  associative-composition-structure-Set hom-set-augmented-simplex-Category
+pr1 associative-composition-structure-augmented-simplex-Category {n} {m} {r} =
+  comp-hom-augmented-simplex-Category {n} {m} {r}
+pr2
+  associative-composition-structure-augmented-simplex-Category {n} {m} {r} {s} =
+  associative-comp-hom-augmented-simplex-Category {n} {m} {r} {s}
+
+id-hom-augmented-simplex-Category :
+  (n : obj-augmented-simplex-Category) → hom-augmented-simplex-Category n n
+id-hom-augmented-simplex-Category n = id-hom-Poset (Fin-Poset n)
+
+left-unit-law-comp-hom-augmented-simplex-Category :
+  {n m : obj-augmented-simplex-Category}
+  (f : hom-augmented-simplex-Category n m) →
+  comp-hom-augmented-simplex-Category {n} {m} {m}
+    ( id-hom-augmented-simplex-Category m)
+    ( f) ＝
+  f
+left-unit-law-comp-hom-augmented-simplex-Category {n} {m} =
+  left-unit-law-comp-hom-Poset (Fin-Poset n) (Fin-Poset m)
+
+right-unit-law-comp-hom-augmented-simplex-Category :
+  {n m : obj-augmented-simplex-Category}
+  (f : hom-augmented-simplex-Category n m) →
+  comp-hom-augmented-simplex-Category {n} {n} {m}
+    ( f)
+    ( id-hom-augmented-simplex-Category n) ＝
+  f
+right-unit-law-comp-hom-augmented-simplex-Category {n} {m} =
+  right-unit-law-comp-hom-Poset (Fin-Poset n) (Fin-Poset m)
+
+is-unital-composition-structure-augmented-simplex-Category :
+  is-unital-composition-structure-Set
+    ( hom-set-augmented-simplex-Category)
+    ( associative-composition-structure-augmented-simplex-Category)
+pr1 is-unital-composition-structure-augmented-simplex-Category =
+  id-hom-augmented-simplex-Category
+pr1 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+  left-unit-law-comp-hom-augmented-simplex-Category {n} {m}
+pr2 (pr2 is-unital-composition-structure-augmented-simplex-Category) {n} {m} =
+  right-unit-law-comp-hom-augmented-simplex-Category {n} {m}
+
+augmented-simplex-Precategory : Precategory lzero lzero
+pr1 augmented-simplex-Precategory = obj-augmented-simplex-Category
+pr1 (pr2 augmented-simplex-Precategory) = hom-set-augmented-simplex-Category
+pr1 (pr2 (pr2 augmented-simplex-Precategory)) =
+  associative-composition-structure-augmented-simplex-Category
+pr2 (pr2 (pr2 augmented-simplex-Precategory)) =
+  is-unital-composition-structure-augmented-simplex-Category
+```
+
+### The augmented simplex category
+
+It remains to be formalized that the augmented simplex category is univalent.
+
+## Properties
+
+### The augmented simplex category is equivalent to the category of finite total orders
+
+This remains to be formalized.

src/category-theory/embedding-maps-precategories.lagda.md

@@ -0,0 +1,88 @@
+# Embedding maps between precategories
+
+```agda
+module category-theory.embedding-maps-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.faithful-maps-precategories
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.injective-maps
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [map](category-theory.maps-precategories.md) between
+[precategories](category-theory.precategories.md) `C` and `D` is an **embedding
+map** if it's an embedding on objects and
+[faithful](category-theory.faithful-maps-precategories.md). Hence embedding maps
+are maps that are embeddings on objects and hom-sets.
+
+Note that for a map of precategories to be called _an embedding_, it must also
+be a [functor](category-theory.functors-precategories.md). This notion is
+considered in
+[`category-theory.embeddings-precategories`](category-theory.embeddings-precategories.md).
+
+## Definition
+
+### The predicate of being an embedding map on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-embedding-map-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-prop-map-Precategory =
+    prod-Prop
+      ( is-emb-Prop (obj-map-Precategory C D F))
+      ( is-faithful-prop-map-Precategory C D F)
+
+  is-embedding-map-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-map-Precategory =
+    type-Prop is-embedding-map-prop-map-Precategory
+
+  is-prop-is-embedding-map-map-Precategory :
+    is-prop is-embedding-map-map-Precategory
+  is-prop-is-embedding-map-map-Precategory =
+    is-prop-type-Prop is-embedding-map-prop-map-Precategory
+```
+
+### The type of embedding maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  where
+
+  embedding-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  embedding-map-Precategory =
+    Σ (map-Precategory C D) (is-embedding-map-map-Precategory C D)
+
+  map-embedding-map-Precategory :
+    embedding-map-Precategory → map-Precategory C D
+  map-embedding-map-Precategory = pr1
+
+  is-embedding-map-embedding-map-Precategory :
+    (e : embedding-map-Precategory) →
+    is-embedding-map-map-Precategory C D (map-embedding-map-Precategory e)
+  is-embedding-map-embedding-map-Precategory = pr2
+```

src/category-theory/embeddings-precategories.lagda.md

@@ -0,0 +1,105 @@
+# Embeddings between precategories
+
+```agda
+module category-theory.embeddings-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import category-theory.embedding-maps-precategories
+open import category-theory.functors-precategories
+open import category-theory.maps-precategories
+open import category-theory.precategories
+
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.embeddings
+open import foundation.equivalences
+open import foundation.propositions
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+A [functor](category-theory.functors-precategories.md) between
+[precategories](category-theory.precategories.md) `C` and `D` is an
+**embedding** if it's an embedding on objects and
+[faithful](category-theory.faithful-functors-precategories.md). Hence embeddings
+are functors that are embeddings on objects and hom-sets.
+
+## Definition
+
+### The predicate of being an embedding on maps between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : map-Precategory C D)
+  where
+
+  is-embedding-prop-map-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-prop-map-Precategory =
+    prod-Prop
+      ( is-functor-prop-map-Precategory C D F)
+      ( is-embedding-map-prop-map-Precategory C D F)
+
+  is-embedding-map-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-map-Precategory =
+    type-Prop is-embedding-prop-map-Precategory
+
+  is-prop-is-embedding-map-Precategory : is-prop is-embedding-map-Precategory
+  is-prop-is-embedding-map-Precategory =
+    is-prop-type-Prop is-embedding-prop-map-Precategory
+```
+
+### The predicate of being an embedding on functors between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  where
+
+  is-embedding-prop-functor-Precategory : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-prop-functor-Precategory =
+    is-embedding-map-prop-map-Precategory C D (map-functor-Precategory C D F)
+
+  is-embedding-functor-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  is-embedding-functor-Precategory =
+    type-Prop is-embedding-prop-functor-Precategory
+
+  is-prop-is-embedding-functor-Precategory :
+    is-prop is-embedding-functor-Precategory
+  is-prop-is-embedding-functor-Precategory =
+    is-prop-type-Prop is-embedding-prop-functor-Precategory
+```
+
+### The type of embeddings between precategories
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2)
+  (D : Precategory l3 l4)
+  where
+
+  embedding-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  embedding-Precategory =
+    Σ (functor-Precategory C D) (is-embedding-functor-Precategory C D)
+
+  functor-embedding-Precategory :
+    embedding-Precategory → functor-Precategory C D
+  functor-embedding-Precategory = pr1
+
+  is-embedding-embedding-Precategory :
+    (e : embedding-Precategory) →
+    is-embedding-functor-Precategory C D (functor-embedding-Precategory e)
+  is-embedding-embedding-Precategory = pr2
+```