Theorems · Definition · category theory

CategoryTheory.MorphismProperty.Under

{T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    CategoryTheory.MorphismProperty T → CategoryTheory.MorphismProperty T → T → Type (max v_1 u_1)

Given a morphism property P on a category T and an object X : T, this is the subcategory of Under X defined by P where morphisms satisfy Q.

Defined in

Mathlib.CategoryTheory.MorphismProperty.Comma

Cited by

43 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category