instPreservesLimitWalkingParallelPairParallelPairMapAAppUnitObjAOfPreservesLimitOfIsCoreflexivePair

English

For a comonad T and a T-coalgebra X, the pair of maps CofreeEqualizer.topMap X and CofreeEqualizer.bottomMap X form an IsCoreflexivePair.

Русский

Для ко-монад T и коалгебры X пары отображений CofreeEqualizer.topMap X и CofreeEqualizer.bottomMap X образуют IsCoreflexivePair.

LaTeX

$$$\text{IsCoreflexivePair} (\mathrm{CofreeEqualizer.topMap} X, \mathrm{CofreeEqualizer.bottomMap} X)$$$

Lean4

instance [PreservesLimitOfIsCoreflexivePair F] :
    ∀ X : Coalgebra adj.toComonad, PreservesLimit (parallelPair (G.map X.a) (NatTrans.app adj.unit (G.obj X.A))) F :=
  fun _ => PreservesLimitOfIsCoreflexivePair.out _ _

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