Theorems · Definition · category theory

CategoryTheory.CatEnriched.hComp

{C : Type u_1} →
  [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    {a b c : CategoryTheory.CatEnriched C} →
      {f f' : a ⟶ b} →
        {g g' : b ⟶ c} →
          (f ⟶ f') → (g ⟶ g') → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g')

The horizontal composition on 2-morphisms is defined using the action on arrows of the composition bifunctor from the enriched category structure.

Defined in

Mathlib.CategoryTheory.Bicategory.CatEnriched

Cited by

13 results in Mathlib

Foundations

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

Assumes

CategoryTheory.EnrichedCategory