English
If G preserves colimits of reflexive pairs and has the same hypotheses as in 75090, then for every X in Algebra adj.toMonad, the parallelPair built from F.map X.a and NatTrans.app adj.counit (F.obj X.A) is preserved by G.
Русский
Если G сохраняет колимиты рефлексивных пар и выполняются условия аналогичные 75090, то для каждого X в Algebra adj.toMonad параллельная пара, построенная из F.map X.a и NatTrans.app adj.counit (F.obj X.A), сохраняется G.
LaTeX
$$$[PreservesColimitOfIsReflexivePair G] \\Rightarrow \\forall X:\\mathrm{Algebra}(adj.toMonad),\\; \\operatorname{PreservesColimit}(\\operatorname{parallelPair}(F.map X.a,\\; \\mathrm{NatTrans.app}\\ adj.counit\\ (F.obj X.A)))\\ G$$$
Lean4
instance [PreservesColimitOfIsReflexivePair G] :
∀ X : Algebra adj.toMonad, PreservesColimit (parallelPair (F.map X.a) (NatTrans.app adj.counit (F.obj X.A))) G :=
fun _ => PreservesColimitOfIsReflexivePair.out _ _
