Structures · Category theory
CategoryTheory.SemiCartesianMonoidalCategory
A monoidal category is semicartesian if the unit for the tensor product is a terminal object.
- Shape
- One type argument · adds isTerminalTensorUnit, fst, snd, fst_def, snd_def
Extends1
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by38
- CategoryTheory.SemiCartesianMonoidalCategory.fst
- CategoryTheory.SemiCartesianMonoidalCategory.snd
- CategoryTheory.SemiCartesianMonoidalCategory.toUnit
- CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit
- CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
- CategoryTheory.SemiCartesianMonoidalCategory.fst_def
- CategoryTheory.SemiCartesianMonoidalCategory.snd_def
- CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc
- CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit
- CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit
- CategoryTheory.AddMonObj.instMonoZero
- CategoryTheory.Mon.instHasZeroObject
- CategoryTheory.Mon.instZeroHom
- CategoryTheory.AddMon.instHasZeroMorphisms
- CategoryTheory.AddMon.zero_hom
- CategoryTheory.AddMon.instZeroHom
- CategoryTheory.Mon.uniqueHomToTrivial
- CategoryTheory.SemiCartesianMonoidalCategory.default_eq_toUnit
- CategoryTheory.uniqueHomToTrivial
- CategoryTheory.MonObj.instIsMonHomOne
- CategoryTheory.AddMonObj.instIsAddMonHomToAddUnit
- CategoryTheory.Mon.zero_hom
- CategoryTheory.MonObj.instMonoOne
- CategoryTheory.SemiCartesianMonoidalCategory.instUniqueHomTensorUnit
- CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory
- CategoryTheory.Mon.instHasZeroMorphisms
- CategoryTheory.AddMonObj.instIsAddMonHomZero
- CategoryTheory.AddMon.instHasZeroObject
- CategoryTheory.AddMon.uniqueHomToTrivial
- CategoryTheory.Mon.isZero_trivial
- CategoryTheory.Functor.chosenProd.fst
- CategoryTheory.AddMon.uniqueHomToTrivial_default_hom
- CategoryTheory.Functor.chosenTerminalIsTerminal
- CategoryTheory.Mon.uniqueHomToTrivial_default_hom
- CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique_iff
- CategoryTheory.Functor.chosenProd.snd
- CategoryTheory.AddMon.isZero_trivial
- CategoryTheory.MonObj.instIsMonHomToUnit