From Category Theory for Programmers - Series 1

Lecture 4 - Terminal and initial objects

• Recap on Kleisli category
• Think of translating a category to a Kleisli category
• Have a category 𝑪 and a Kleisli category
• For every object in 𝑪, the object is in the Kleisli category
• But the arrows in 𝑪 are not the same as the arrows in the Kleisli category
• From last time, arrows change the type a to (a, string)
• Call this new object m a
• (preview of things to come, this re-mapping is called a functor)
• In this example, composition of these other types can translate to composition in the Kleisli category
• In 𝑪, and Kleisli
• a → m a ⇒ id_a in Kleisli
• a → m b ⇒ a → b in Kleisli
• This 'a → m a' is a monad
• Universal construction
• Define a singleton set
• Has an arrow from any other set
• For example (in Haskell) the Unit function, which ignores any input and produces Unit ( )
• Or object Bool
• Has at least two arrows from any other object: true, false
• Singleton set is a terminal object
• Defined by incoming arrows
• A terminal object in a category is an object that has a unique arrow coming from any other object
• Which is two different conditions (In Haskell)
• ∀ a ∃ 𝑓 :: a → ( )
• ∀ 𝑓 :: a → ( ), ∀ 𝑔 :: a → ( ) ⇒ 𝑓 = 𝑔
• Not every category has a terminal object
• For example, categories with order, there might not be a largest or smallest element
• Empty set can be defined by outgoing arrows
• (In Haskell) for every type a, there is an "absurd" function: Void → a
• Initial object
• Has a unique outgoing arrow to every object
• (In Haskell)
• ∀ a ∃ 𝑓 :: Void → a
• ∀ 𝑓 :: Void → a, ∀ 𝑔 :: Void → a ⇒ 𝑓 = 𝑔
• In set corresponds to the empty set
• No matter what path you take to the terminal object, it can be shrunk to a single unique arrow
• Universal construction
• Given a pattern
• Is ranked by incoming arrows
• So an object with more incoming arrows is "better" than another object

(part 2)

• A terminal object can have outgoing arrows
• Every construction in category theory can be given by reversing arrows
• Called "opposite" category
• For example
• Category 𝑪
• a → b
• With the arrow 𝑓
• The opposite is
• Category 𝑪^op
• b → a
• With the arrow 𝑓^op
• Taking the opposite category means the order of composition is inverted
• (𝑔 ∘ 𝑓)^op = 𝑓^op ∘ 𝑔^op
• What's the category version of cartesian product?
• What are properties of cartesian product?
• For every pair of objects in a cartesian product, there are two mappings "fst" and "snd" (first and second)
• a ⨯ b, fst to a, snd to b
• As a category object
• An object with two arrows to two other objects
• What's the universal construction ranking of cartesian product?
• Same as before, better rank has arrow to it
• Given graph
• p:: c → a
• q:: c → b
• m:: c` → c
• p`:: c` → a
• q`:: c` → b
• c is better than c`, given that there is a morphism m, such that
• p ∘ m = p`
• q ∘ m = q`
• Haskell
• Given type (a,b)
• fst(a, _) = a
• snd(_, b) = b
• (note, "_" is wildcard type)
• Categorical product of a,b is a third object c with two projections
• p:: c → a
• q:: c → b
• For any other categorical product c` there is a unique morphism
• m :: c`→ c
• p ∘ m = p`
• q ∘ m = q`
• Not every category has products
• Might not have products for every pair