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

→

#

instead of talking about elements in category theory, we can talk about the function from unit

→

#

bool = in SET Category, set with two elements

→

Ideas from [[category theory]]