Theorems · Theorem · category theory

CommMonCat.coyonedaType_obj_map

∀ (X : Type uᵒᵖ) {X_1 Y : CommMonCat} (f : X_1 ⟶ Y),
  (CommMonCat.coyonedaType.obj X).map f =
    CommMonCat.ofHom (MonoidHom.pi fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i))

Defined in

Mathlib.Algebra.Category.MonCat.Yoneda

Cited by

0 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound