Theorems · Theorem · category theory

CategoryTheory.ForgetEnrichment.homTo_id

∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : CategoryTheory.ForgetEnrichment W C),
  CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)

The identity in the "underlying" category of an enriched category.

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.EnrichedCategory