Theorems · Definition · category theory

CategoryTheory.Over.mapComp

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y Z : T} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) ≅
            (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)

The natural isomorphism arising from mapComp_eq.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category