Theorems · Definition · category theory
CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit
{C : Type u} →
{inst : CategoryTheory.Category.{v, u} C} →
[self : CategoryTheory.SemiCartesianMonoidalCategory C] →
CategoryTheory.Limits.IsTerminal (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)The tensor unit is a terminal object.
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 25 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.Categorystatement and proof · cited by 32,673
- CategoryTheory.MonoidalCategoryStruct.tensorUnitstatement · cited by 1,384
- CategoryTheory.Limits.IsTerminalstatement · cited by 153
- CategoryTheory.SemiCartesianMonoidalCategorystatement and proof · cited by 14
Cited by35
Results whose statement or proof uses this declaration.
- CategoryTheory.SemiCartesianMonoidalCategory.toUnitproof · cited by 103
- CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fstproof · cited by 24
- CategoryTheory.CartesianMonoidalCategory.whiskerLeft_sndproof · cited by 19
- CategoryTheory.CartesianMonoidalCategory.whiskerRight_sndproof · cited by 16
- CategoryTheory.SemiCartesianMonoidalCategory.fst_defstatement · cited by 13
- CategoryTheory.CartesianMonoidalCategory.whiskerRight_fstproof · cited by 13
- CategoryTheory.SemiCartesianMonoidalCategory.snd_defstatement · cited by 10
- CategoryTheory.CartesianMonoidalCategory.preservesTerminalIsoproof · cited by 8
- CategoryTheory.CartesianMonoidalCategory.associator_hom_fstproof · cited by 8
- CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_fstproof · cited by 7
- CategoryTheory.CartesianMonoidalCategory.braiding_hom_fstproof · cited by 7
- CategoryTheory.CartesianMonoidalCategory.braiding_hom_sndproof · cited by 7