Theorems · Definition · category theory

CategoryTheory.MorphismProperty.Over.mkIdTerminal

{T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [inst_1 : P.ContainsIdentities] →
          CategoryTheory.Limits.IsTerminal
            (CategoryTheory.MorphismProperty.Over.mk ⊤ (CategoryTheory.CategoryStruct.id X) ⋯)

X ⟶ X is the terminal object of P.Over ⊤ X.

Defined in

Mathlib.CategoryTheory.Limits.MorphismProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.ContainsIdentities