Theorems · Definition · category theory
CategoryTheory.Cat.chosenTerminal
CategoryTheory.Cat
The chosen terminal object in Cat.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
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.Discreteproof · cited by 2,447
- CategoryTheory.Catstatement · cited by 884
- CategoryTheory.Cat.ofproof · cited by 189
- CategoryTheory.ULiftHomproof · cited by 15
Cited by8
Results whose statement or proof uses this declaration.
- CategoryTheory.Cat.fromChosenTerminalEquivstatement and proof · cited by 2
- SSet.Truncated.HomotopyCategory.isoTerminalstatement · cited by 2
- SSet.hoFunctor.unitHomEquivstatement · cited by 1
- SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitalitystatement and proof · cited by 0
- CategoryTheory.Cat.chosenTerminalIsTerminalstatement · cited by 0
- SSet.hoFunctor.unitHomEquiv_eqstatement · cited by 0
- SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitalitystatement and proof · cited by 0
- CategoryTheory.Monoidal.tensorUnitstatement · cited by 0