Unit

📁 Source: Mathlib/CategoryTheory/Limits/Unit.lean

Statistics

Metric	Count
Definitions punitCocone, punitCoconeIsColimit, punitCone, punitConeIsLimit	4
Theorems instHasColimitsOfSizeDiscretePUnit, instHasLimitsOfSizeDiscretePUnit	2
Total	6

CategoryTheory.Limits

Definitions

Name	Category	Theorems
punitCocone 📖	CompOp	—
punitCoconeIsColimit 📖	CompOp	—
punitCone 📖	CompOp	—
punitConeIsLimit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitsOfSizeDiscretePUnit 📖	mathematical	—	HasColimitsOfSize CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—
instHasLimitsOfSizeDiscretePUnit 📖	mathematical	—	HasLimitsOfSize CategoryTheory.Discrete CategoryTheory.discreteCategory	—	—

---

← Back to Index