mapPair — Mathlib

English

There exists a natural transformation between two functors out of the walking pair, specified by its components f and g at left and right, respectively, satisfying naturality.

Русский

Существует натурализованное преобразование между двумя функторaми из WalkingPair, заданное компонентами f и g на левом и правом respectively, удовлетворяющее условию натуральности.

LaTeX

$$$$ \exists \eta: F \Rightarrow G,\ \eta_{left}=f,\ \eta_{right}=g,\ \text{naturality holds}. $$$$

Lean4

/-- The natural transformation between two functors out of the
walking pair, specified by its components. -/
def mapPair : F ⟶ G
    where
  app
    | ⟨left⟩ => f
    | ⟨right⟩ => g
  naturality := fun ⟨X⟩ ⟨Y⟩ ⟨⟨u⟩⟩ => by cat_disch

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