Theorems · Definition · category theory

CategoryTheory.EnrichedCategory.Hom

{V : Type v} →
  {inst : CategoryTheory.Category.{w, v} V} →
    {inst_1 : CategoryTheory.MonoidalCategory V} →
      {C : Type u₁} → [self : CategoryTheory.EnrichedCategory V C] → C → C → V

X ⟶[V] Y is the V object of morphisms from X to Y.

Defined in

Mathlib.CategoryTheory.Enriched.Basic

Cited by

114 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CategoryTheory.EnrichedCategory