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