Theorems · Definition · category theory

CategoryTheory.Under.equivalenceOfIsInitial

{T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Limits.IsInitial X → (CategoryTheory.Under X ≌ T)

If X : T is initial, then the under category of X is equivalent to T.

Defined in

Mathlib.CategoryTheory.Comma.Over.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category