Theorems · Definition · category theory

CategoryTheory.Over.equivalenceOfIsTerminal

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

If X : T is terminal, then the over 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