Theorems · Theorem · category theory

CategoryTheory.CatEnriched.id_eq

∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] (X : CategoryTheory.CatEnriched C),
  CategoryTheory.CategoryStruct.id X = (CategoryTheory.eId CategoryTheory.Cat X).toFunctor.obj { down := { as := () } }

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.EnrichedCategory