Enrichment
This enrichment formalization is not so much meaningful according to nlab.
Rather study Homotopy Type Theory, or pure type theory.
# (-2)-category (nothing)
A (-2)-category is an element of (-2)Cat.
But there is no element in (-2)Cat.
Only "there is no element in (-2)Cat." might define a unique element.
# (-1)-category (small)
a (-1)-category is an element of (-1)Cat.
Only 2 (-1)-category exists.
- $ \top $ ( $ := $ `(-2)Cat` )
- $ \bot $
# 0-category (small)
so, a 0-category is a set.
e.g.
- `Bool` ( := `(-1)Cat = ` { $ \top $ , $ \bot $ } )
- $ \emptyset $
- { $ * $ } : a set with unique element
# 1-category (small)
a 1-category is a category.
~~~
- 0-morphism
- 1-morphism
- identity
- composition
- associativity
- unit
~~~
e.g.
- `0 Cat := Sets`
- $ Mon $
- $ Vect _ {\mathbb{K}} $
a category is small if its objects are sets.
# 2-category / bicategory (large)
A 2-category or bicategory is a category which has 2-morphisms equipped with a kind of tensor categories (or monoidal categories).
~~~
- 0-morphism
- 1-morphism
- 2-morphism
- identity
- composition
- associativity
- unit
~~~
## tensor category / monoidal category
A tensor category is denoted as ( $ C $ , $ \otimes $ , $ 1 $ , $ \alpha $ , $ \lambda $ , $ \rho $ ) where ;
- $ C $ : category
- $ \otimes $ : $ C \times C \to C $ : tensor product functor
- $ 1 $ $ \in $ Ob( $ C $ ) : identity object
- $ \alpha $ : $ ( - \otimes - ) \otimes - \Rightarrow - \otimes ( - \otimes - ) $ : associator ( isomorphism )
- $ \lambda $ : $ 1 \otimes - \Rightarrow - $ : left unitor ( isomorphism )
- $ \rho $ : $ - \otimes 1 \Rightarrow - $ : right unitor ( isomorphism )
s.t.
- pentagon diagram (associative law)
- triangle diagram (unit law)
are satisfied.
## e.g.
- `1 Cat := Cat` : `Cat` itself is a bicategory so it is large
# double category (large)
a double category is a category which is a litte modified 2-category.
# 3-category / tricategory (large)
# 4-catefory / tetracategory (large)
# n-category
~~~
- 0-morphism := object
- 1-morohism := morphism : object -> object
- 2-morphism := nat : morphism -> morphism
- 3-morphism := so on ...
~~~
# groupoid G : many objects category
which has 2 Functors
~~~
comp : G(x,y) x G(y,z) -> G(x,z)
inv : G(x,y) -> G(y,x)
~~~
# monoid : one object category
which has 2 Functors
# small & large
~~~
3 classification of objects
- set
- type
- category
a category is small if object is a set
a category is large otherwise (i.e. type, category)
~~~