English
There exists a colimit for a certain parallel pair built from F, G, and adjoint counits, expressed via a coequalizer.
Русский
Существует колимит для заданной параллельной пары, построенной из F, G и counit-образов adjoint, выраженный через коэквалайзер.
LaTeX
$$$\\text{HasColimit}\\bigl(\\text{parallelPair}(F\\mapsto G\\mapsto \\mathrm{counit.app}, \\mathrm{counit.app} )\\bigr) = \\operatorname{HasCoequalizer}(F.map A.a, adj.counit.app (F.obj A.A))$$$
Lean4
instance [∀ A : adj.toMonad.Algebra, HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] (B : D) :
HasColimit (parallelPair (F.map (G.map (NatTrans.app adj.counit B))) (NatTrans.app adj.counit (F.obj (G.obj B)))) :=
inferInstanceAs <|
HasCoequalizer (F.map ((comparison adj).obj B).a) (adj.counit.app (F.obj ((comparison adj).obj B).A))
