English
If G reflects colimits of split pairs, then for any A,B in D and any f,g: A ⟶ B that form a split pair, G reflects the colimit of the parallel pair parallelPair f g.
Русский
Если G отражает колимиты распавшихся пар, то для любых объектов A,B в D и любых f,g: A ⟶ B, образующих распадаемую пару, G отражает колимит диаграммы parallelPair f g.
LaTeX
$$\\forall A,B:\\,\\mathrm{Hom}(A,B),\\\\[G.IsSplitPair f g] \\Rightarrow \\operatorname{ReflectsColimit}(\\operatorname{parallelPair} f g)\\ G$$
Lean4
instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [ReflectsColimitOfIsSplitPair G] :
ReflectsColimit (parallelPair f g) G :=
ReflectsColimitOfIsSplitPair.out f g
