instPreservesColimitWalkingParallelPairParallelPairOfIsSplitPairOfPreservesColimitOfIsSplitPair

English

A collection of auxiliary instances relating (co)limits and splits that support the main results about monadicity and adjunctions.

Русский

Набор вспомогательных экземпляров, связывающих (ко)лимиты и разрезы, поддерживающих основные результаты о монадамике и сопряжениях.

LaTeX

$$$\\text{Auxiliary\_instances: }\\text{HasCoequalizerOfIsSplitPair}, \\text{PreservesColimitsOfShape}, \\text{IsSplitPair}$$$

Lean4

instance {A B} (f g : A ⟶ B) [G.IsSplitPair f g] [PreservesColimitOfIsSplitPair G] :
    PreservesColimit (parallelPair f g) G :=
  PreservesColimitOfIsSplitPair.out f g

Похожие утверждения