/
simplex-category.lagda.md
167 lines (133 loc) · 5.78 KB
/
simplex-category.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
# The simplex category
```agda
module category-theory.simplex-category where
```
<details><summary>Imports</summary>
```agda
open import category-theory.composition-operations-on-binary-families-of-sets
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 simplex category** is the category consisting of inhabited finite total
orders 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 (succ-ℕ n)` to `Fin (succ-ℕ 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 simplex precategory
```agda
obj-simplex-Category : UU lzero
obj-simplex-Category = ℕ
hom-set-simplex-Category :
obj-simplex-Category → obj-simplex-Category → Set lzero
hom-set-simplex-Category n m =
hom-set-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
hom-simplex-Category :
obj-simplex-Category → obj-simplex-Category → UU lzero
hom-simplex-Category n m = type-Set (hom-set-simplex-Category n m)
comp-hom-simplex-Category :
{n m r : obj-simplex-Category} →
hom-simplex-Category m r → hom-simplex-Category n m → hom-simplex-Category n r
comp-hom-simplex-Category {n} {m} {r} =
comp-hom-Poset
( Fin-Poset (succ-ℕ n))
( Fin-Poset (succ-ℕ m))
( Fin-Poset (succ-ℕ r))
associative-comp-hom-simplex-Category :
{n m r s : obj-simplex-Category}
(h : hom-simplex-Category r s)
(g : hom-simplex-Category m r)
(f : hom-simplex-Category n m) →
comp-hom-simplex-Category {n} {m} {s}
( comp-hom-simplex-Category {m} {r} {s} h g)
( f) ＝
comp-hom-simplex-Category {n} {r} {s}
( h)
( comp-hom-simplex-Category {n} {m} {r} g f)
associative-comp-hom-simplex-Category {n} {m} {r} {s} =
associative-comp-hom-Poset
( Fin-Poset (succ-ℕ n))
( Fin-Poset (succ-ℕ m))
( Fin-Poset (succ-ℕ r))
( Fin-Poset (succ-ℕ s))
inv-associative-comp-hom-simplex-Category :
{n m r s : obj-simplex-Category}
(h : hom-simplex-Category r s)
(g : hom-simplex-Category m r)
(f : hom-simplex-Category n m) →
comp-hom-simplex-Category {n} {r} {s}
( h)
( comp-hom-simplex-Category {n} {m} {r} g f) ＝
comp-hom-simplex-Category {n} {m} {s}
( comp-hom-simplex-Category {m} {r} {s} h g)
( f)
inv-associative-comp-hom-simplex-Category {n} {m} {r} {s} =
inv-associative-comp-hom-Poset
( Fin-Poset (succ-ℕ n))
( Fin-Poset (succ-ℕ m))
( Fin-Poset (succ-ℕ r))
( Fin-Poset (succ-ℕ s))
associative-composition-operation-simplex-Category :
associative-composition-operation-binary-family-Set hom-set-simplex-Category
pr1 associative-composition-operation-simplex-Category {n} {m} {r} =
comp-hom-simplex-Category {n} {m} {r}
pr2 associative-composition-operation-simplex-Category {n} {m} {r} {s} =
is-associative-witness-associative-composition-operation-binary-family-Set
( hom-set-simplex-Category)
( comp-hom-simplex-Category)
( associative-comp-hom-simplex-Category)
id-hom-simplex-Category : (n : obj-simplex-Category) → hom-simplex-Category n n
id-hom-simplex-Category n = id-hom-Poset (Fin-Poset (succ-ℕ n))
left-unit-law-comp-hom-simplex-Category :
{n m : obj-simplex-Category} (f : hom-simplex-Category n m) →
comp-hom-simplex-Category {n} {m} {m} (id-hom-simplex-Category m) f ＝ f
left-unit-law-comp-hom-simplex-Category {n} {m} =
left-unit-law-comp-hom-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
right-unit-law-comp-hom-simplex-Category :
{n m : obj-simplex-Category} (f : hom-simplex-Category n m) →
comp-hom-simplex-Category {n} {n} {m} f (id-hom-simplex-Category n) ＝ f
right-unit-law-comp-hom-simplex-Category {n} {m} =
right-unit-law-comp-hom-Poset (Fin-Poset (succ-ℕ n)) (Fin-Poset (succ-ℕ m))
is-unital-composition-operation-simplex-Category :
is-unital-composition-operation-binary-family-Set
( hom-set-simplex-Category)
( comp-hom-simplex-Category)
pr1 is-unital-composition-operation-simplex-Category = id-hom-simplex-Category
pr1 (pr2 is-unital-composition-operation-simplex-Category) {n} {m} =
left-unit-law-comp-hom-simplex-Category {n} {m}
pr2 (pr2 is-unital-composition-operation-simplex-Category) {n} {m} =
right-unit-law-comp-hom-simplex-Category {n} {m}
simplex-Precategory : Precategory lzero lzero
pr1 simplex-Precategory = obj-simplex-Category
pr1 (pr2 simplex-Precategory) = hom-set-simplex-Category
pr1 (pr2 (pr2 simplex-Precategory)) =
associative-composition-operation-simplex-Category
pr2 (pr2 (pr2 simplex-Precategory)) =
is-unital-composition-operation-simplex-Category
```
### The simplex category
It remains to be formalized that the simplex category is univalent.
## Properties
### The simplex category is equivalent to the category of inhabited finite total orders
This remains to be formalized.
### The simplex category has a face map and degeneracy unique factorization system
This remains to be formalized.
### The simplex category has a degeneracy and face map unique factorization system
This remains to be formalized.
### There is a unique nontrivial involution on the simplex category
This remains to be formalized.