StrictSegal

Statistics

Metric	Count
Definitions	0
Theorems `quasicategory`, `quasicategory'`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`quasicategory` 📖	mathematical	—	`SSet.Quasicategory`	—	`SSet.quasicategory_of_filler` `spineInjective` `SSet.Path.ext'` `CategoryTheory.types_comp_apply` `CategoryTheory.NatTrans.naturality` `SSet.spine_arrow` `spine_δ_arrow_lt` `SSet.Subcomplex.yonedaEquiv_coe` `CategoryTheory.Subfunctor.lift_ι` `SSet.stdSimplex.map_apply` `Quiver.Hom.unop_op` `SSet.stdSimplex.yonedaEquiv_map` `Equiv.apply_symm_apply` `SimplexCategory.mkOfSucc_δ_lt` `spine_δ_arrow_gt` `SimplexCategory.mkOfSucc_δ_gt` `Fintype.complete` `SSet.stdSimplex.ext` `spine_δ_arrow_eq` `spineToSimplex_spine_apply` `SimplexCategory.mkOfSucc_δ_eq`
`quasicategory'` 📖	mathematical	—	`SSet.Quasicategory`	—	`quasicategory`

---