Cartesian

📁 Source: Mathlib/CategoryTheory/CopyDiscardCategory/Cartesian.lean

Statistics

Metric	Count
Definitions instComonObjOfCartesian, ofCartesianMonoidalCategory	2
Theorems instDeterministic, instIsCommComonObjOfCartesian	2
Total	4

CategoryTheory.CartesianCopyDiscard

Definitions

Name	Category	Theorems
instComonObjOfCartesian 📖	CompOp	1 math math: instIsCommComonObjOfCartesian
ofCartesianMonoidalCategory 📖	CompOp	1 math math: instDeterministic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDeterministic 📖	mathematical	—	CategoryTheory.Deterministic CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory ofCartesianMonoidalCategory	—	CategoryTheory.counit_eq_toUnit CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit CategoryTheory.comul_eq_lift CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.Category.comp_id CategoryTheory.CartesianMonoidalCategory.lift_map CategoryTheory.Category.id_comp
instIsCommComonObjOfCartesian 📖	mathematical	—	CategoryTheory.IsCommComonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory instComonObjOfCartesian	—	CategoryTheory.comul_eq_lift CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom

---

← Back to Index