Theorems · Theorem · category theory

CategoryTheory.CostructuredArrow.w

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {X Y : CategoryTheory.CostructuredArrow S T} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (S.map f.left) Y.hom = X.hom

Defined in

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category