StrictBicategory

📁 Source: Mathlib/AlgebraicTopology/Quasicategory/StrictBicategory.lean

Statistics

Metric	Count
Definitions QCat, bicategory, catEnrichedOrdinaryCategory, equiv	4
Theorems strictBicategory	1
Total	5

SSet

Definitions

Name	Category	Theorems
QCat 📖	CompOp	1 math math: QCat.strictBicategory

SSet.QCat

Definitions

Name	Category	Theorems
bicategory 📖	CompOp	1 math math: strictBicategory
catEnrichedOrdinaryCategory 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictBicategory 📖	mathematical	—	CategoryTheory.Bicategory.Strict SSet.QCat bicategory	—	CategoryTheory.CatEnrichedOrdinary.instStrict

SSet.QCat.forgetEnrichment

Definitions

Name	Category	Theorems
equiv 📖	CompOp	—

---

← Back to Index