Understanding the classical monad-theory
correspondence
Nathan Corbyn
University of Oxford

MSFP 08.07.2024

Objective

Objective• Prove the equivalence:
Law ≃ Mndfin (Set)Objective• ProveUnderstand the equivalence:
Law ≃ Mndfin (Set)

Plan

Plan

• Take three steps:

Plan• Take three steps:
Law ≃ ProMnd× (Fop )≃ RMnd(F ,→ Set)
≃ Mndfin (Set)Plan• Take three steps:
Law ≃ ProMnd× (Fop )≃ RMnd(F ,→ Set)
≃ Mndfin (Set)• Although not necessary to write down a proof, hopefully these
all feel very natural by the end!

Plan

• Take three steps:
Law ≃ ProMnd× (Fop )≃ RMnd(F ,→ Set)
≃ Mndfin (Set)• Although not necessary to write down a proof, hopefully these
all feel very natural by the end!
• Arkor’s thesis takes this approach in extreme generality

Outline
Part I
Lawvere theories
Cartesian promonads
Law ≃ ProMnd× (Fop )Part II
Finitary monads
Relative monads
RMnd(F ,→ Set) ≃ Mndfin (Set)Part III
ProMnd× (Fop ) ≃ RMnd(F ,→ Set)

Part I

Lawvere theories

Lawvere theories• Presentation invariant descriptions of algebraic theories

Lawvere theories• Presentation invariant descriptions of algebraic theories• Can be quite tricky to wrap your head aroundLawvere theories• Consider a presentation of the theory of monoids:Lawvere theories• Consider a presentation of the theory of monoids:
u:0

⊕:2

Lawvere theories• Consider a presentation of the theory of monoids:
⊕:2

u:0

u⊕x=x
x⊕u =x(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)

Lawvere theories• We get lots of derivable operations

Lawvere theories• We get lots of derivable operations—e.g.,x ⊕ (y ⊕ (z ⊕ w))x⊕x(u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w)

Lawvere theories• We get lots of derivable operations—e.g.,x ⊕ (y ⊕ (z ⊕ w))x⊕x(u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w)

• Some of these are provably equalLawvere theories• We get lots of derivable operations—e.g.,x ⊕ (y ⊕ (z ⊕ w))x⊕x(u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w)

• Some of these are provably equal:x ⊕ x = (u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w) = x ⊕ (y ⊕ (z ⊕ w))

Lawvere theories• We get lots of derivable operations—e.g.,x ⊕ (y ⊕ (z ⊕ w))x⊕x(u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w)

• Some of these are provably equal:x ⊕ x = (u ⊕ x) ⊕ (x ⊕ u)(x ⊕ y) ⊕ (z ⊕ w) = x ⊕ (y ⊕ (z ⊕ w))• Important: Copying and discarding of variables is allowedLawvere theories

Lawvere theories• Lawvere’s idea: no matter how you present the theory, thesame operations should be derivable and satisfy the same
equationsLawvere theories• Lawvere’s idea: no matter how you present the theory, thesame operations should be derivable and satisfy the same
equations• A Lawvere theory bundles derivable operations and theirequations into a categoryLawvere theories

Lawvere theories• What does this look like?

Lawvere theories• What does this look like?
• For each n ∈ N, write down the set of derivable operations inat most n variables, modulo provable equality:
T (n, 1)

Lawvere theories• What does this look like?
• For each n ∈ N, write down the set of derivable operations inat most n variables, modulo provable equality:
T (n, 1)

• Extend this to all m ∈ N taking
T (n, 0) = {⋆}T (n, m + 1) = T (n, m) × T (n, 1)

Lawvere theories• What does this look like?
• For each n ∈ N, write down the set of derivable operations inat most n variables, modulo provable equality:
T (n, 1)

• Extend this to all m ∈ N taking
T (n, 0) = {⋆}T (n, m + 1) = T (n, m) × T (n, 1)• In other words, T (n, m) consists of tuples of m operations
each in (at most) n variables

Lawvere theories

Lawvere theories• Idea: T (−, =) describes the hom-sets of a category.

Lawvere theories• Idea: T (−, =) describes the hom-sets of a category.
• Composition is substitution!

Lawvere theories• Idea: T (−, =) describes the hom-sets of a category.
• Composition is substitution!

T (n, m)| {z }

×m operations in n variables

T (m, 1)| {z }

1 operation in m variables↓
T (n, 1)| {z }

substitute the m variables for the m derived operations

Lawvere theories

Lawvere theories• We get more than just a category, we get a cartesian categoryLawvere theories• We get more than just a category, we get a cartesian category:⟨xi ⟩i∈n⟨xi+n ⟩i∈mn ←−−−− n + m −−−−−→ m

⟨⟩

n−
→0

Lawvere theories• We get more than just a category, we get a cartesian category:⟨xi ⟩i∈n⟨xi+n ⟩i∈mn ←−−−− n + m −−−−−→ m

⟨⟩

n−
→0

• This is intimately connected with the fact that we’ve allowed
variables to be copied and discarded

Relationship to FopRelationship to Fop• Call F the category with objects n ∈ N and morphisms
F(n, m) = n → m

Relationship to Fop• Call F the category with objects n ∈ N and morphisms
F(n, m) = n → m• Claim: Fop corresponds to the Lawvere theory determined by
the empty presentation:

Relationship to Fop• Call F the category with objects n ∈ N and morphisms
F(n, m) = n → m• Claim: Fop corresponds to the Lawvere theory determined by
the empty presentation:◦ The only derivable operations are the variables

Relationship to Fop• Call F the category with objects n ∈ N and morphisms
F(n, m) = n → m• Claim: Fop corresponds to the Lawvere theory determined by
the empty presentation:◦ The only derivable operations are the variables:T∅ (n, 1) = n∼= F(1, n)Relationship to Fop• Call F the category with objects n ∈ N and morphisms
F(n, m) = n → m• Claim: Fop corresponds to the Lawvere theory determined by
the empty presentation:◦ The only derivable operations are the variables:T∅ (n, 1) = n∼= F(1, n)◦ Extending,T∅ (n, 0) = {⋆} ∼= F(0, n)T∅ (n, m + 1) = T∅ (n, m) × T∅ (n, 1)∼= F(m, n) × F (1, n)∼= F(m + 1, n)

Relationship to FopRelationship to Fop• If we have two presentations Θ ⊆ Θ′ , we get a (unique)corresponding identity-on-objects functor TΘ → TΘ′Relationship to Fop• If we have two presentations Θ ⊆ Θ′ , we get a (unique)corresponding identity-on-objects functor TΘ → TΘ′◦ Hand-waving: All the operations derivable in the old theory arestill derivable in the new theory, but might be identified via the
new equations

Relationship to Fop• If we have two presentations Θ ⊆ Θ′ , we get a (unique)corresponding identity-on-objects functor TΘ → TΘ′◦ Hand-waving: All the operations derivable in the old theory arestill derivable in the new theory, but might be identified via the
new equations• In particular, we always have a (unique) identity-on-objects
functorFop → TΘ

Relationship to Fop• If we have two presentations Θ ⊆ Θ′ , we get a (unique)corresponding identity-on-objects functor TΘ → TΘ′◦ Hand-waving: All the operations derivable in the old theory arestill derivable in the new theory, but might be identified via the
new equations• In particular, we always have a (unique) identity-on-objects
functorFop → TΘ
• Moreover, this functor will always preserve products strictlyRelationship to Fop• If we have two presentations Θ ⊆ Θ′ , we get a (unique)corresponding identity-on-objects functor TΘ → TΘ′◦ Hand-waving: All the operations derivable in the old theory arestill derivable in the new theory, but might be identified via the
new equations• In particular, we always have a (unique) identity-on-objects
functorFop → TΘ
• Moreover, this functor will always preserve products strictly• We can use this to define Lawvere theories semantically!

Semantic definition

Semantic definition• Definition: a Lawvere theory is a category T equipped with astrictly product-preserving identity-on-objects functor
J : Fop → TSemantic definition• Definition: a Lawvere theory is a category T equipped with astrictly product-preserving identity-on-objects functor
J : Fop → T• We obtain a category Law of Lawvere theories and triangles:
F

T

T′
J′

J

Fop

Promonads

Promonads• Definition: A promonad is a monoid in the category ofendoprofunctors on a category C

Promonads• Definition: A promonad is a monoid in the category ofendoprofunctors on a category C

Promonads

Promonads• Definition: A promonad is a profunctor P : C op × C → Set
equipped with maps
Z c:C
µ:

P(−, c) × P(c, =) → P(−, =)η : C(−, =) → P(−, =)subject to...

Promonads• Definition: A promonad is a profunctor P : C op × C → Set
equipped with maps
Z c:C
µ:

P(−, c) × P(c, =) → P(−, =)η : C(−, =) → P(−, =)subject to...

Promonads

Promonads• Promonads are an extremely useful way to build new
categories from old ones

Promonads• Promonads are an extremely useful way to build new
categories from old ones
• Promonads show up everywhere but aren’t given the credit
they deserve

Promonads

Promonads• Say we have some category C

Promonads• Say we have some category C• We love the objects of C

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:◦ Missing some maps

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:◦ Missing some maps
◦ Not enough equations

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:◦ Missing some maps
◦ Not enough equations◦ Still important though!

Promonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:◦ Missing some maps
◦ Not enough equations◦ Still important though!

• Promonads are a technical tool for describing the morphisms
we wish we had and how they relate to the morphisms we’ve
got right nowPromonads• Say we have some category C• We love the objects of C
• But the morphisms are a bit of a disappointment:◦ Missing some maps
◦ Not enough equations◦ Still important though!

• Promonads are a technical tool for describing the morphisms
we wish we had and how they relate to the morphisms we’ve
got right now• If we set things up properly, we get a new category D with thesame objects as C and an identity-on-objects functor C → D

Promonads

Promonads• How do we do this?

Promonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set

Promonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set◦ For each x, y ∈ C, P(x, y ) is the hom-set you wish you had

Promonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set◦ For each x, y ∈ C, P(x, y ) is the hom-set you wish you had◦ The functorial actions tell you how to compose your dream
maps with your disappointments

Promonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set◦ For each x, y ∈ C, P(x, y ) is the hom-set you wish you had◦ The functorial actions tell you how to compose your dream
maps with your disappointments• Ask for a natural transformation
η : C(−, =) → P(−, =)Promonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set◦ For each x, y ∈ C, P(x, y ) is the hom-set you wish you had◦ The functorial actions tell you how to compose your dream
maps with your disappointments• Ask for a natural transformation
η : C(−, =) → P(−, =)◦ Every disappointment has something to live up toPromonads• How do we do this?
• Start with a profunctor P(−, =) : C op × C → Set◦ For each x, y ∈ C, P(x, y ) is the hom-set you wish you had◦ The functorial actions tell you how to compose your dream
maps with your disappointments• Ask for a natural transformation
η : C(−, =) → P(−, =)◦ Every disappointment has something to live up to◦ Not necessarily injective

Promonads

Promonads• We’ve also got to explain how to compose our ideal maps

Promonads• We’ve also got to explain how to compose our ideal maps
• For each c ∈ C we want to say we have a naturaltransformation:µc : P(−, c) × P(c, =) → P(−, =)Promonads• We’ve also got to explain how to compose our ideal maps
• For each c ∈ C we want to say we have a naturaltransformation:µc : P(−, c) × P(c, =) → P(−, =)• But it’s a bit more subtle!

Promonads• We need all our composition operations to line up with eachotherPromonads• We need all our composition operations to line up with eachother:xcc′yPromonads• We need all our composition operations to line up with eachother:xcc′y• The fancy way to say this is that we have a single naturaltransformation
Z c:Cµ:P(−, c) × P(c, =) → P(−, =)Promonads

Promonads• Finally, we need a couple of laws to hold:Promonads• Finally, we need a couple of laws to hold:◦ Composition should be associative

Promonads• Finally, we need a couple of laws to hold:◦ Composition should be associative◦ Lifting and composing should agree with acting

Promonads• Finally, we need a couple of laws to hold:◦ Composition should be associative◦ Lifting and composing should agree with acting

P(−, c) × C(c, =)P(−,c)×ηc◁c

P(−, c) × P(c, =)µc

P(−, =)

Promonads• Finally, we need a couple of laws to hold:◦ Composition should be associative◦ Lifting and composing should agree with acting

P(−, c) × C(c, =)P(−,c)×ηc◁c

P(−, c) × P(c, =)µc

P(−, =)• We get a category ProMnd(C) whose objects are promonads
on C and morphisms are natural transformations which
respect the composition and liftingPromonads

Promonads• What’s this bought us?

Promonads• What’s this bought us?
• We certainly get a functor:
ProMnd(C) → (C/Cat)ioo

Promonads• What’s this bought us?
• We certainly get a functor:
ProMnd(C) → (C/Cat)ioo• In fact, we get an equivalence:
ProMnd(C) ≃ (C/Cat)ioo

Cartesian promonads

Cartesian promonads• You may have spotted, we’ve got the following:
Law = (Fop /Cat)ioo,× ,→ (Fop /Cat)ioo ≃ ProMnd(Fop )Cartesian promonads• You may have spotted, we’ve got the following:
Law = (Fop /Cat)ioo,× ,→ (Fop /Cat)ioo ≃ ProMnd(Fop )• Can we restrict the right-hand side to get an equivalence?

Cartesian promonads

Cartesian promonads• We only want to consider promonads which induce cartesianfunctors

Cartesian promonads• We only want to consider promonads which induce cartesianfunctors• Consider (P : F × Fop → Set, µ, η) a promonad on Fop

Cartesian promonads• We only want to consider promonads which induce cartesianfunctors• Consider (P : F × Fop → Set, µ, η) a promonad on Fop• Because the induced functor is identity-on-objects, it will
strictly preserve products iff our dream maps still validate theuniversal properties

Cartesian promonads• We only want to consider promonads which induce cartesianfunctors• Consider (P : F × Fop → Set, µ, η) a promonad on Fop• Because the induced functor is identity-on-objects, it will
strictly preserve products iff our dream maps still validate theuniversal properties• In other words,
P(−, 0) ∼=⊤∼P(−, n + m) = P(−, n) × P(−, m)naturally in m and n

Cartesian promonads

P(−, 0) ∼=⊤P(−, n + m) ∼= P(−, n) × P(−, m)Cartesian promonads

P(−, 0) ∼=⊤P(−, n + m) ∼= P(−, n) × P(−, m)• Key point: this is the same as asking that the curried functor
P : F → [Fop , Set]
lands in cartesian functors

Cartesian promonads

P(−, 0) ∼=⊤P(−, n + m) ∼= P(−, n) × P(−, m)• Key point: this is the same as asking that the curried functor
P : F → [Fop , Set]
lands in cartesian functors• We want cartesian profunctors:
P : F → [Fop , Set]×

The first equivalenceThe first equivalence

Law ≃ ProMnd× (Fop )Part II

Monads

Monads• A monad is a monoid in the category of endofunctors on acategory C

Monads• A monad is a monoid in the category of endofunctors on acategory C

Monads

Monads• A monad is a lax 2-functor 1 → Cat

Monads• A monad is a lax 2-functor 1 → Cat

Monads

Monads• Monads are a technical tool for describing algebraic structuresinternal to general categories

Monads• Monads are a technical tool for describing algebraic structuresinternal to general categories• Rather than take a syntactic approach, monads arefundamentally semantically motivatedMonads• Monads are a technical tool for describing algebraic structuresinternal to general categories• Rather than take a syntactic approach, monads arefundamentally semantically motivated• The monad-theory correspondence for Set essentially says thatthe semantic approach and the syntactic approach are secretly
the same

Monads• Monads are a technical tool for describing algebraic structuresinternal to general categories• Rather than take a syntactic approach, monads arefundamentally semantically motivated• The monad-theory correspondence for Set essentially says thatthe semantic approach and the syntactic approach are secretly
the same• Mumble mumble technicalities...

Monads

Monads• Fundamental observation: an algebra is an object equippedwith some operations we can somehow evaluate

Monads• Fundamental observation: an algebra is an object equippedwith some operations we can somehow evaluate• Take an object x ∈ C, what does it mean to evaluate in x?

Monads• Fundamental observation: an algebra is an object equippedwith some operations we can somehow evaluate• Take an object x ∈ C, what does it mean to evaluate in x?
• Choose another object Tx ∈ C of ‘computations’ and a map
a : Tx → x

Monads

Monads• How do we make sure we’ve chosen a sensible notion ofcomputation?

Monads• How do we make sure we’ve chosen a sensible notion ofcomputation?
• First, we make T : C → C an endofunctor:

Monads• How do we make sure we’ve chosen a sensible notion ofcomputation?
• First, we make T : C → C an endofunctor:◦ The notion of computation should be independent of thespecific x I’ve chosen

Monads• How do we make sure we’ve chosen a sensible notion ofcomputation?
• First, we make T : C → C an endofunctor:◦ The notion of computation should be independent of thespecific x I’ve chosen◦ Functoriality says that T can’t ‘see’ xMonads

Monads• If we’ve already got a (generalised) element of x, we shouldhave a ‘do nothing’ computation:
ηx : x → Tx

Monads• If we’ve already got a (generalised) element of x, we shouldhave a ‘do nothing’ computation:
ηx : x → Tx

• Similarly, if I have a computation that computes acomputation, this should reduce to a single computation thatworks out what it needs to do and does it:µx : TTx → Tx

Monads• If we’ve already got a (generalised) element of x, we shouldhave a ‘do nothing’ computation:
ηx : x → Tx

• Similarly, if I have a computation that computes acomputation, this should reduce to a single computation thatworks out what it needs to do and does it:µx : TTx → Tx

• These should be natural (again, we shouldn’t look at x):
η : 1C → Tµ : TT → T

Monads

Monads• The monad laws express three more sensible properties ofcomputation when you think in these terms!

Monads• The monad laws express three more sensible properties ofcomputation when you think in these terms!
Tx

ηTx

1Tx

TTx
µx

Tx

T (ηx )1Tx

Tx

Monads• The monad laws express three more sensible properties ofcomputation when you think in these terms!
Tx

ηTx

1Tx

TTx
µx

Tx

T (ηx )

1Tx

Tx

TTTx

T (µx )

µTx

TTx

TTx
µx

µx

Tx

Monads• The monad laws express three more sensible properties ofcomputation when you think in these terms!
Tx

ηTx

1Tx

TTx
µx

Tx

T (ηx )

1Tx

Tx

TTTx

T (µx )

µTx

TTx

TTx
µx

µx

Tx

• We get a category Mnd(C) whose objects are monads on C
and whose morphisms are natural transformations preserving
all the structureFinitary monads

Finitary monads• Disclaimer: this part is quite technical, so I’m going to brushover a lot of details, but hopefully the picture still comes out!

Finitary monads

Finitary monads• We’re not always interested in notions of computation in themost general senseFinitary monads• We’re not always interested in notions of computation in themost general sense• Sometimes we want to ensure that our computations are
somehow ‘finitely describable’:Finitary monads• We’re not always interested in notions of computation in themost general sense• Sometimes we want to ensure that our computations are
somehow ‘finitely describable’:◦ If we have a monad T on Set, we might hope that acomputation c ∈ TX can be described using at most finitely
many elements of X

Finitary monads• We’re not always interested in notions of computation in themost general sense• Sometimes we want to ensure that our computations are
somehow ‘finitely describable’:◦ If we have a monad T on Set, we might hope that acomputation c ∈ TX can be described using at most finitely
many elements of X
◦ For example, computations might be formal sums of at mostfinitely many elements

Finitary monads• We’re not always interested in notions of computation in themost general sense• Sometimes we want to ensure that our computations are
somehow ‘finitely describable’:◦ If we have a monad T on Set, we might hope that acomputation c ∈ TX can be described using at most finitely
many elements of X
◦ For example, computations might be formal sums of at mostfinitely many elements• If we’re looking for a connection with universal algebra, this iscertainly a sensible restriction!

Finitary monads• Category theory gives us some very technical, but very useful,
notions of finiteness in general categories• As we’re only really interested in monads on Set today:◦ A monad T on Set is finitary iff for every set X and elementc ∈ TX , there is a finite subset i : X0 ↣ X through which c
factors:
c

{⋆}
c0

TX
Ti

TX0
• We’ll call the full subcategory of Mnd(Set) spanned byfinitary monads Mndfin (Set)• It only really matters what T does to finite sets!

Relative monads

Relative monads• A monad relative to a functor J : C → E is a monoid in the
skew-monoidal category ([C, E], ◦J , J)

Relative monads• A monad relative to a functor J : C → E is a monoid in the
skew-monoidal category ([C, E], ◦J , J)

Relative monads

Relative monads• Relative monads are a technical tool for describing notions ofcomputation constrained to some particular diagram in a
category

Relative monads• Relative monads are a technical tool for describing notions ofcomputation constrained to some particular diagram in a
category• The computations might form objects in a much larger
category, but are only described for a (potentially) smaller
system of objects

Relative monads

Relative monads• What does this look like?

Relative monads• What does this look like?
• First, pick your system of objects J : C → E

Relative monads• What does this look like?
• First, pick your system of objects J : C → E• For each object x ∈ C, define the computations Tx ∈ ERelative monads• What does this look like?
• First, pick your system of objects J : C → E• For each object x ∈ C, define the computations Tx ∈ E• Again, we want ‘do nothing’ computations
ηx : Jx → Tx

Relative monads

Relative monads• This time, we can’t necessarily build computations thatcompute computations

Relative monads• This time, we can’t necessarily build computations thatcompute computations• However, we can introduce a mechanism for sequencing
computations(−)† : E(Jx, Ty ) → E(Tx, Ty )

Relative monads• This time, we can’t necessarily build computations thatcompute computations• However, we can introduce a mechanism for sequencing
computations(−)† : E(Jx, Ty ) → E(Tx, Ty )◦ I find it helps to think of maps Jx → Ty as computations witha ‘parameter’Relative monads

Relative monads• Similar to monads, we have some sensible properties we
expect to hold

Relative monads• Similar to monads, we have some sensible properties we
expect to hold(ηx )† = 1Tx

Relative monads• Similar to monads, we have some sensible properties we
expect to hold(ηx )† = 1Tx
Tx
f†

ηx

Jx

f

Ty

Relative monads

Relative monads

f

Jx

Ty

g†

(g † f )†

Tx

Tz
g†

f†

Ty

Tz

Relative monads

f

Jx

Ty

g†

(g † f )†

Tx

Tz

Tz
g†

f†

Ty
• These laws automatically guarantee functoriality of T andnaturality of η and (−)† !

Relative monads

f

Jx

Ty

g†

(g † f )†

Tx

Tz

Tz
g†

f†

Ty
• These laws automatically guarantee functoriality of T andnaturality of η and (−)† !
• For each J : C → E, we get a category RMnd(J) of monads
relative to J and natural transformations preserving thestructure

The second equivalenceThe second equivalenceRMnd(F ,→ Set) ≃ Mndfin (Set)The picture

The picture

Set
LanJ T

J

F

T

Set

Part IIIThe third equivalenceThe third equivalence

ProMnd× (Fop ) ≃ RMnd(F ,→ Set)

What we’ve got

What we’ve got• P : F → [Fop , Set]×

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set• η:J→T

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set• η:J→T• (−)† : Set(J(−), T (=)) → Set(T (−), T (=))

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set• η:J→T• (−)† : Set(J(−), T (=)) → Set(T (−), T (=))• ...

Key ingredientKey ingredient[Fop , Set]× ≃ Set

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set ≃ [Fop , Set]×

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set ≃ [Fop , Set]×• η:J→T

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set ≃ [Fop , Set]×• η : J → T η : Fop (−, =) → T• (−)† : Set(J(−), T (=)) → Set(T (−), T (=))

What we’ve got• P : F → [Fop , Set]×• η : Fop (−, =) → P• µ : ∫ c:C P(−, c) × P(c, =) → P• ...

• T : F → Set ≃ [Fop , Set]×• η : J → T η : Fop (−, =) → T• (−)† : Set(J(−), T (=)) → Set(T (−), T (=))
T (m, n) ∼= [Fop , Set]× (Fop (n, −), Tm) → [Fop , Set]× (Tn, Tm)

SummarySummary• We’ve covered a lot of ground:Summary• We’ve covered a lot of ground:◦ Lawvere theories

Summary• We’ve covered a lot of ground:◦ Lawvere theories◦ Finitary monads

Summary• We’ve covered a lot of ground:◦ Lawvere theories◦ Finitary monads◦ Relative monads

Summary• We’ve covered a lot of ground:◦ Lawvere theories◦ Finitary monads◦ Relative monads◦ Promonads

Summary• We’ve covered a lot of ground:◦ Lawvere theories◦ Finitary monads◦ Relative monads◦ Promonads◦ Ways these all link up!

Summary• We’ve covered a lot of ground:◦ Lawvere theories◦ Finitary monads◦ Relative monads◦ Promonads◦ Ways these all link up!

• Hopefully you’ve got some intuitions for some of these andcan go away and look at the details

References
Thorsten Altenkirch, James Chapman, and Tarmo Uustalu.
Monads need not be endofunctors.
Lecture Notes in Computer Science (including subseries Lecture
Notes in Artificial Intelligence and Lecture Notes in
Bioinformatics), 6014 LNCS:297–311, 2010.
Nathanael Arkor.
Monadic and higher-order structure.
2022.
F. William Lawvere.
Functorial semantics of algebraic theories and some algebraic
problems in the context of functorial semantics of algebraic
theories, 1963.