Universal Construction | Category Theory and Why We Care 1.2

To fully utilise the exciting category theory we've learnt so far, we need a way to abstract definitions from a specific category and then be able to apply them in any category we want. The solution to this is universal construction.

This video will explore the process of universal construction and see it used in practice, which will further expose some elegant relationships between categories that we've seen before. Taking examples from mathematical proofs, functional programming and beyond, this is the next major step into abstraction that our category theory journey takes us.

― Timestamps ―

0:00 - Intro
1:03 - Isomorphism
5:22 - Terminal object
10:41 - Universal construction
12:27 - Conjunction
17:32 - Product
18:29 - Pair type
24:12 - Outro
25:00 - Exercise

― Credits ―

All animation and voiceover created by Eyesomorphic.
Background music: 'Sonder', composed by Caleb Peppiatt.

― Further Reading ―

Category Theory and Why We Care, by Eyesomorphic (Lecture series):    • Category Theory and Why We Care  
Algebra: Chapter 0 (Book), by Paulo Aluffi