Theorems · Definition · category theory
CategoryTheory.Limits.IsTerminal.ofUniqueHom
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{Y : C} → (h : (X : C) → X ⟶ Y) → (∀ (X : C) (m : X ⟶ Y), m = h X) → CategoryTheory.Limits.IsTerminal YAn object Y is terminal if for every X there is a unique morphism X ⟶ Y
(as explicit arguments).
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- Uniqueproof · cited by 400
- CategoryTheory.Limits.IsTerminalstatement · cited by 153
- CategoryTheory.Limits.IsTerminal.ofUniqueproof · cited by 0
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.Over.cartesianMonoidalCategoryproof · cited by 68
- CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategoryOverproof · cited by 49
- CategoryTheory.Limits.FormalCoproduct.isTerminalInclproof · cited by 9
- CategoryTheory.Functor.isTerminalConstproof · cited by 8
- CategoryTheory.Sheaf.isTerminalTerminalproof · cited by 4
- CategoryTheory.Over.rightUnitor_inv_left_fstproof · cited by 2
- CategoryTheory.Limits.IsInitial.opproof · cited by 2
- CategoryTheory.SubobjectRepresentableBy.isTerminalΩ₀proof · cited by 1
- CategoryTheory.Over.rightUnitor_inv_left_sndproof · cited by 1
- SSet.stdSimplex.isTerminalObj₀proof · cited by 1
- CategoryTheory.Over.leftUnitor_inv_left_fstproof · cited by 1
- CategoryTheory.Over.leftUnitor_inv_left_sndproof · cited by 1