from bartosz milewski category theory lectures
exploring Universal Constructions
void = initial object = in set category, empty set = in logic, proving “false”
initial object = for every point in a category there is one and only one arrow from the initial object to the point
identity exists, void -> void
nothing can return void
anything that takes in a void can return any type, void -> a
unit = terminal object = () = in set category, set with one element = in logic, proving “true”
terminal object = from every point in a category, there is one and only one arrow to the terminal object
two terminal objects are always have a uniquely ismorphic = only one way to isomorph between the two
you can return a unit from anything, a -> ()
can use unit to define the element of a set, one :: () -> int, two :: () -> int
as many unit -> t functions exist as elements in the type t
unit -> t
instead of talking about elements in category theory, we can talk about the function from unit
bool = in set category, set with two elements
TODO how are groups, rings, fields defined as a category?