English
The standard extensionality lemma for CatCospanTransform morphisms: if two transformations have equal left, right, and base components, then they are equal as morphisms in CatCospanTransform.
Русский
Лемма экстенсиональности для морфизмов CatCospanTransform: если левый, правый и базовый компоненты двух преобразований равны, то сами преобразования равны как морфизмы CatCospanTransform.
LaTeX
$$$ \\theta = \\theta' \\;\\text{ if } \\theta.left = \\theta'.left, \\; \\theta.right = \\theta'.right, \\theta.base = \\theta'.base $$$
Lean4
/-- The square `transformObjPrecomposeObjSquare` respects identities. -/
theorem transformObjPrecomposeObjSquare_iso_hom_id {X : Type u₇} {Y : Type u₈} [Category.{v₇} X] [Category.{v₈} Y]
(U : X ⥤ Y) (F : A ⥤ B) (G : C ⥤ B) :
(CatCommSq.iso (transform Y |>.obj <| .id F G) (precompose F G |>.obj U) (precompose F G |>.obj U)
(transform X |>.obj <| .id F G)).hom ≫
whiskerLeft (precompose F G |>.obj U) (transformObjId X F G).hom =
whiskerRight (transformObjId Y F G).hom (precompose F G |>.obj U) ≫
(precompose F G |>.obj U).leftUnitor.hom ≫ (precompose F G |>.obj U).rightUnitor.inv :=
by cat_disch
