prodComparison_snd — Mathlib

English

In a cartesian monoidal category, applying F to a pair (A,B) and then projecting with snd is the same as applying F to snd(A,B).

Русский

В картианской моноидальной категории применение F к паре (A,B) и затем проекция snd равны применению F к snd(A,B).

LaTeX

$$$$ \mathrm{prodComparison} F A B \; \circ \; \mathrm{snd} (F.obj A) (F.obj B) = F.map (\mathrm{snd} A B). $$$$

Lean4

@[reassoc (attr := simp)]
theorem prodComparison_snd : prodComparison F A B ≫ snd _ _ = F.map (snd A B) :=
  lift_snd _ _

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