Theorems · Definition · category theory
CategoryTheory.Limits.terminal.from
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.Limits.HasTerminal C] → (P : C) → P ⟶ ⊤_ CThe map from an object to the terminal object.
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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 · cited by 32,603
- CategoryTheory.Limits.HasTerminalstatement and proof · cited by 142
- CategoryTheory.Limits.terminalstatement · cited by 141
- CategoryTheory.Functor.emptyproof · cited by 103
- CategoryTheory.Limits.limit.liftproof · cited by 48
- CategoryTheory.Limits.asEmptyConeproof · cited by 12
Cited by99
Results whose statement or proof uses this declaration.
- HomotopicalAlgebra.IsFibrantproof · cited by 56
- AlgebraicGeometry.AffineSpaceproof · cited by 51
- CategoryTheory.Limits.terminalIsTerminalproof · cited by 31
- CategoryTheory.Limits.terminal.comp_fromstatement and proof · cited by 21
- prodIsoPullbackstatement · cited by 13
- CategoryTheory.subterminalsEquivMonoOverTerminalproof · cited by 8
- CategoryTheory.Limits.prod.leftUnitorproof · cited by 7
- AlgebraicGeometry.AffineSpace.toSpecMvPolyproof · cited by 7
- CategoryTheory.Limits.prod.rightUnitorproof · cited by 7
- limitConeOfTerminalAndPullbacksproof · cited by 6
- SSet.Augmented.stdSimplexproof · cited by 5