Documentation
InfinityCosmos
.
ForMathlib
.
AlgebraicTopology
.
Quasicategory
.
Basic
Search
return to top
source
Imports
Init
Mathlib.AlgebraicTopology.Quasicategory.Basic
Imported by
SSet
.
QCat
SSet
.
instCategoryQCat
source
def
SSet
.
QCat
:
Type
(u_1 + 1)
Equations
SSet.QCat
=
CategoryTheory.FullSubcategory
SSet.Quasicategory
Instances For
source
instance
SSet
.
instCategoryQCat
:
CategoryTheory.Category.{u_1, u_1 + 1}
QCat
Equations
SSet.instCategoryQCat
=
CategoryTheory.FullSubcategory.category
SSet.Quasicategory