§ Monads from Riehl
 I'm having some trouble enmeshing my haskell intuition for monads with the rigor, so this
 A category is said to be monadi is an expository note to bridge the gap.
§ What is a monad
 A monad is an endofunctor
T: C > C
equipped with two natural transformations:  (1)
return/eta: idC => T
[yeeta, since we are yeeting into the monad. ]  (2)
join/mu: T^2 => T
, such that two laws are obeyed:
 First law:
mu, T
commutation:
T^3(x) T(@mu@x)> T^2@x
 
mu@(T@x) mu@x
 
v v
T^2(x)mu@x> T(x)
 Second law:
mu, eta
cancellation:
(Tx) eta@(T@x)> T^2(x)
EQ 
 
T@(eta@x) mu@x
 
v EQv
T^2(x)mu@x> T(x)

mu . eta T = mu . T eta = 1
§ Monad from adjunction
 Any adjunction between a Free functor
F: L > H
and a forgetfUl/Underlying functor U: H > L
F  U
gives a monad. The categories are named L, H
for lo, high
in terms of the amount of structure they have. We go from low structure to high structure by the free functor.  The monad on
L
is given by T := UF
.  Recall that an adjunction gives us
pullback: (F l > h) > (l > U h)
and pushfwd: (l > U h) > (F l > h)
. The first is termed pullback since it takes a function living in the high space and pulls it back to the low space.  This lets us start with
(F l > F l)
, peel a F
from the left via pullback
to create (l > U (F l))
. That is we have return: l > T l
.  In the other direction, we are able to start with
(U h > U h)
, peel a U
from the right via pushforward
to create (F U h > h)
. This allows us to create the counit as T^2 l = F U F U l = F (U F) U l > F U l = T l
.
§ Algebra for a monad $C^T$.
 Any monad, given by
(T: C > C, return: 1C => T, join: T^2 => T)
has a category of T
algebras associated to it.  The objects of
Talg
are morphisms f: Tc > c
.  The morphisms of
Talg
between f: Tc > c
and g: Td > d
are commuting squares, determined by an arr: c > d
Tc T arr> Td
 
f g
 
v v
c arr> d
 The notation for the category as $C^T$ makes some sense, since it consists of objects of the form
Tc > c
which matches somewhat with the function notation. We should have written $C^{TC}$ but maybe that's too unweildy.
§ Factoring of forgetful functor of adjunction
 Any adjunction
(F: L > H, U: H > L)
with associated monad T
allows us to factor U: H > L
as:
H Stx> L^T forget> L
 So we write elements of
H
in terms of syntax/"algebra over L
". We then forget the algebra structure to keep only the low form.  The way to think about this is that any object in the image of
U
in fact has a (forgotten) algebra structure, which is why we can first go to L^T
and then forget the algebraic structure to go back to L
. It might be that this transition from H
to L^T
is very lossy. This means that the algebra is unable to encode what is happening in H
very well.
§ Monadic adjunction
 Let us consider an adjunction
(F: L > H, U: H > L)
with monad T
. Factor U
via L^T
as:
H Stx> L^T forget> L
 The adjunction is said to be monadic if in the factoring of
U
via L^T
, it happens that H ~= L^T
. That is, Stx
is an equivalence between H
and L^T
.  The way to think about this is that any object in the image of
U
in fact has a (forgotten) algebra structure, and this algebra structure actually correctly represents everything that was happening in H
.  Another way to say the adjunction
F: L > H: U
is monadic is to say that is that F
is monadic over U
. We imagine the higher category H
and the free functor F
lying over L
and U
.  Warning : This is a STRONGER condition than saying that
UF
is a monad. UF
is ALWAYS a monad for ANY adjunction. This says that H ~= L^T
, via the factoring H Stx> L^T forget> L
.  We sometimes simply say that
U
is monadic , to imply that there exists an F
such that UF
is an adjunction and that U ~= L^T
.
§ Category of models for an algebraic theory
 A functor is finitary if it preserves filtered colimits.
 In particular, a monad
T : L > L
is finitary if it preserves filtered colimits in C.  If a right adjoint is finitary, then so is its monad because its left adjoint preserves all colimits. Thus, their composite preserves filtered colimits.
 A category
H
is a category of models for an algebraic theory if there is a finitary monadic functor U : H > Set
.
§ Limits and colimits in categories of algebras
 We say that
H
is monadic over L
iff the adjunction F: L > H: U
such that the monad T: L > L := UF
gives rise to an equivalence of categories H ~= L^T
.
§ Riehl: Limits and colimits in categories of algebras
Here, we learn theorems about limits and colimits in L^T
.
§ Lemma 5.6.1: If U
is monadic over F
, then U
reflects isos
 That is, if for some
f: h > h'
, if Uf: Uh > Uh'
is an iso, then so is f
.  Since the adjunction
F  U
is a monadic adjunction ( U
is monadic over F
), we know that H ~= L^T
, and U
equals the forgetful functor (H = L^T) > L
.  Write the arrow
f: h > h'
as an arrow in L^T
via the commuting square datum determined by g: h > h'
:
TlTg>Tl'
 
a a'
 
v v
lg>l'
 Since we assume that
U(Tg)
is iso, this means that g
is iso. This means that there exists a g'
which is the inverse of g
. But this means that the diagram below commutes:
Tl<Tg'Tl'
 
a a'
 
v v
l<g'l'
 For a proof, we see that
a' . Tg = g . a'
. Composing by g'
on left, giving: g' . a' . Tg = a'
. Composing by Tg'
on the right, we get: g'. a' = a' . Tg'
. That's the statement of the above square.  This means we have created an inverse
Tg'
, which reflects g'
into L^T
.
§ Corollary 5.6.2: Bijective continuous functions in CHaus are isos
 When we forget to
Set
, we see that bijections are the isos. Thus, in CHaus
(compact haussdorff spaces) which is monadic over Set
, we have that the arrows that forget to become isos in set, ie, continuous bijections are also isos.
§ Corollary 5.6.4: Any bĳective homomorphism arising from a monadic adjunction which forgets to Set
will be iso
 Follow the exact same proof.
§ Thm 5.6.5.i A monadic functor U: H > L
creates any limits that L
has.
 Since the equivalence
H ~= L^T
creates all limits/colimits, it suffices to show the result for U^T: L^T > L
.  Consider a diagram
D: J > C^T
with image spanned by (T(D[j]) f[j]> D[j])
.  Consider the forgotten diagram
U^TD: J > C
with image spanned by D[j]
. Create the limit cone P
(for product, since product is limit) with morphisms pi[j]: P > D[j]
. We know this limit exists since we assume that L
has this limit that U^T
needs to create.  We can reinterpret the diagram
D: J > C^T
as a natural transformation between two functors Top, Bot: J > C
. These functors are Top(j) := T(D[j])
, Bottom(j) := D[j]
.  The the natural transformation is given by
eta: Top => Bottom
, with defn eta(j) := D[j]f[j]> D[j]
where f[j]
is given by the image of (T(D[j]) f[j]> D[j])
.  So we see that
eta: Top => Bot
can also be written as eta: TD => D
since Top ~= TD
and Bot ~= D
.  Now consider the composition of natural transformations
Const(TL) =Tpi=> TD =gamma=> D
all in J > C
. This gives us a cone with summit TL
.  This cone with summit
TL
factors through L
via the unique morphism lambda: TL > L
. We wish to show that (TL lambda> L)
is a T
algebra, and is the limit of D
.  Diagram chase. Ugh.
§ Corollary 5.6.6: The inclusion of a reflective subcategory creates all limits
 The inclusion of a reflective subcategory is monadic.
 This lets us create all limits by the above proposition.
§ Corollary 5.6.7: Any category monadic over Set
is complete

Set
has all limits.  The forgetful functor
U: H > L
creates all limits that L=Set
has.  Thus
H
has all limits, ie. is complete.
§ Corollary 5.6.9: Set
is cocomplete
 The contravariant power set functor
P: Set^op > Set
is monadic. 
Set
has all limits, and P
creates all limits.  Thus all limits of
Set^op
exist, ie, all colimits of Set
exist.
§ Category of models for alg. theory is complete
TODO
§ Category of algebras has coproducts
 We show how to construct the free product of monoids via haskell. The same principle generalizes for any algebraic theory:
import Control.Monad(join)
eval :: Monoid a => Monoid b => [Either [a] [b]] > [Either a b]
eval = map (either (Left . mconcat) (Right . mconcat))
transpose :: Either [a] [b] > [Either a b]
transpose = either (map Left) (map Right)
flatten :: [Either [a] [b]] > [Either a b]
flatten = join . map transpose
§ If $T: C \to C$ is finitary and $C$ is complete and cocomplete, then so is $C^T$
 We have already seen that if $C$ is complete then so is $C^T$
 We have also seen that $C^T$ contains coproducs
 So is we show that $C^T$ has coequalizers, then we get cocomplete, since any colimit can be expressed as coproductcoequalizer.
 To show that all coequalizers exists is to show that there is an adjoint to the functor
const: [C^T] > [J > C^T]
where J := [a f,g> b]
is the diagram category for coequalizers.  Recall that the adjoint sends a diagram
[J > C^T]
to the nadir that is the coequalizer in C^T
.  See that the constant functor trivially preserves limits.
 To show that it possesses an adjunction, we apply an adjoint functor theorem (fuck me). In particular, we apply the general adjoint functor theorem, so we must show that the solution set condition is satisfied.
 Recall that the solution set condition for $F: C \to D$ requires that for each $d \in D$, the comma category $const(d) \downarrow F$ admit weakly initial objects.
 Unwrapping that definition: For each $d \in D$, there is a solution set. Tht is, there exists a small set $I$and a family of objects $c_I$ and a family of morphisms $f_I: d \to F(c_i)$ such that any morphism $d \to F(c)$ in $D$ can be factored via some $f_i$ as $d \xrightarrow{f_I} F(c_i) \xrightarrow{g} F(c) = d \to F(c)$.
 To apply the theorem, we must produce a solution set for every object in
[J > C^T]
, that is, for each parallel pair of morphisms $f, g: (A, \alpha) \to (B, \beta)$.  We will produce a solution set with a single element by creating a fork $(Q, u)$ such that any other fork factors through this fork (perhaps non uniquely!) So we create:
$(A, \alpha) \xrightarrow{f, g} (B, \beta) \xrightarrow{q} (Q, u)$
 If we know how to create coequalizers in $C^T$, then this would be easy: we literally just create a coequalizer.
 Instead, we create some "approximation" of the coequalizer with $(Q, u)$.
 To start with, we define $q_0: B \to Q_0$ in $C$ of the pair $(A \xrightarrow{f, g} B$).
 If $Tq_0$ would be the coequalizer of $Tf, Tg$ then we are done. But this is unlikely, since a monad need not preserve coequalizers.
 Instead, we simply calculate the coequalizer of $Tf, Tg$ and call this $q_1: B \to Q_1=TQ_0$.
 Repeat inductively to form a directed limit (colimit).
 Monad preserves filtered colimits, since in $UF$, $F$ the left adjoint preserves all colimits, and $U$the right adjoint preserves colimits since it simply forgets the data in