Theorems · Theorem · category theory

CategoryTheory.Comon.ComonToMonOpOp_map

∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Comon C} (f : X ⟶ Y),
  (CategoryTheory.Comon.ComonToMonOpOp C).map f = Opposite.op { hom := f.hom.op, isMonHom_hom := ⋯ }

Defined in

Mathlib.CategoryTheory.Monoidal.Comon_

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory