Theorems · Theorem · category theory
CategoryTheory.Limits.IsTerminal.hom_ext
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (t : CategoryTheory.Limits.IsTerminal X)
(f g : Y ⟶ X), f = gAny two morphisms to a terminal object are equal.
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 27 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.
Cites4
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
- CategoryTheory.Limits.IsTerminalstatement and proof · cited by 153
- CategoryTheory.Limits.IsLimit.hom_extproof · cited by 43
Cited by32
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.IsTerminal.comp_fromproof · cited by 13
- CategoryTheory.Limits.IsTerminal.from_selfproof · cited by 9
- AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparatedproof · cited by 3
- isPullbackOfIsTerminalIsProductstatement · cited by 3
- SSet.Quasicategory.hasLiftingPropertyproof · cited by 2
- TopCat.Presheaf.isSheaf_of_isTerminal_of_indiscreteproof · cited by 2
- CategoryTheory.Limits.IsTerminal.strict_hom_extproof · cited by 2
- SSet.quasicategory_of_hasLiftingPropertyproof · cited by 2
- CategoryTheory.Functor.final_const_of_isTerminalproof · cited by 1
- CategoryTheory.CostructuredArrow.IsUniversal.hom_descproof · cited by 1
- CategoryTheory.Subobject.Classifier.χ_pullback_obj_mk_truth_arrowproof · cited by 1
- CategoryTheory.Endofunctor.Coalgebra.Terminal.right_inv'proof · cited by 1