instHasEqualizerMapAAppUnitObjAOfHasEqualizerOfIsCosplitPair

English

For A, there is a limit for the parallel pair built from G.map A.a and adj.unit.app (G.obj A.A) under the given conditions preserving the limit.

Русский

Для A существует предел параллельной пары, построенной из G.map A.a и adj.unit.app (G.obj A.A) при заданных условиях сохранения предела.

LaTeX

$$$\operatorname{HasLimit}\left(\operatorname{parallelPair}(G.map A.a) (adj.unit.app (G.obj A.A))\right).$$$

Lean4

instance [HasEqualizerOfIsCosplitPair F] :
    ∀ (A : Coalgebra adj.toComonad), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A)) := fun _ =>
  HasEqualizerOfIsCosplitPair.out F _ _

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