A Categorical View of Adjunctions, Free Constructions, and Profunctor Optics
summary
Adjunctions become the practical tool for deriving universal properties and free constructions (lists, free monoids, free groups) by exhibiting explicit isomorphisms between hom-sets; profunctor optics arise from treating homs as contravariant×covariant → Set and composing monoidal actions to get concrete optics like lenses and prisms; traversals map to Taylor series of types via applicative/monoidal structure; the claim that a monad Phi left adjoint to Theta generates all optics is stated and illustrated with Haskell-flavored constructions and worked examples.
AI-written summary · about
chapters (4)
- 0:00Start
- 13:43Free Monroy Construction on Sets
- 28:19The Universal Property of Products
- 30:59Universal Cones
related talks
01h 00mProspects for Computer Formalization of Infinite-Dimensional Category Theory
01h 02mTheory and Models of Lambda Calculus Untyped and Typed - Part 4 of 5
33mTheory and Models of Lambda Calculus Untyped and Typed - Part 5 of 5
10mHomomorphic Reverse Differentiation of Iteration
41mWar Time Proofs and Futuristic Programs
04mSeparated and Shared Effects in Higher-Order Languages
22mBook Of Monads: An Interview
13mTyped Abstractions for Causal Probabilistic Programming