16 lines
428 B
Agda
16 lines
428 B
Agda
module Trinitarianism.AsCats where
|
||
|
||
{-
|
||
Here are some things that we could like to have in a category
|
||
(in which we want to do maths e.g. the category of sets)
|
||
* Initial objects (empty set)
|
||
* Terminal objects (singleton)
|
||
* Sums
|
||
* Products
|
||
* Cartesian closed (for two objects A B, maps A → B
|
||
are also an object in the category)
|
||
* Natural numbers object (the natural numbers ℕ in Set)
|
||
* and maybe more
|
||
|
||
-}
|