Structures · Category theory
CategoryTheory.FinallySmall
A category is FinallySmall.{w} if there is a final functor from a w-small category.
- Shape
- One type argument · adds final_smallCategory
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- Prod
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- CategoryTheory.fromFinalModel
- CategoryTheory.FinalModel
- CategoryTheory.FinallySmall.exists_small_weakly_terminal_set
- CategoryTheory.FinallySmall.fromFilteredFinalModel
- CategoryTheory.finallySmall_of_final_of_finallySmall
- CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall
- CategoryTheory.FinallySmall.exists_of_isFiltered
- CategoryTheory.Limits.isIndObject_of_isFiltered_of_finallySmall
- CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel
- CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel
- CategoryTheory.FinallySmall.final_smallCategory
- CategoryTheory.instFinallySmallProd
- CategoryTheory.final_fromFinalModel
- CategoryTheory.instInitiallySmallOppositeOfFinallySmall
- CategoryTheory.FinallySmall.preservesColimitsOfShape_of_isFiltered
- CategoryTheory.smallCategoryFinalModel
- CategoryTheory.FinallySmall.FilteredFinalModel
- CategoryTheory.FinallySmall.instCategoryFilteredFinalModel
- CategoryTheory.FinalModel.congr_simp
Ancestors0
No ancestors.