English
Let D have reflexive coequalizers and G reflect isomorphisms. For any reflexive pair f,g: A ⟶ B in any category, if G preserves colimits for reflexive pairs, then G preserves the colimit of parallelPair f g.
Русский
Пусть в D существуют рефлексивные пары эквализации, и G отображает изоморфизмы. Тогда для любой рефлексивной пары f,g: A ⟶ B сохранение колимита параллельной пары parallelPair f g выполняется для G.
LaTeX
$$[IsReflexivePair f g] \\Rightarrow [PreservesColimitOfIsReflexivePair G] \\Rightarrow \\operatorname{PreservesColimit}(\\operatorname{parallelPair} f g)\\ G$$
Lean4
instance {A B} (f g : A ⟶ B) [IsReflexivePair f g] [PreservesColimitOfIsReflexivePair G] :
PreservesColimit (parallelPair f g) G :=
PreservesColimitOfIsReflexivePair.out f g
