Session Category3
View
theory dependencies
View
document
View
outline
Theories
Category
EpiMonoIso
DualCategory
ConcreteCategory
InitialTerminal
Functor
Subcategory
SetCategory
SetCat
ProductCategory
NaturalTransformation
BinaryFunctor
FunctorCategory
Yoneda
Adjunction
EquivalenceOfCategories
FreeCategory
DiscreteCategory
Limit
CategoryWithPullbacks
CartesianCategory
CategoryWithFiniteLimits
CartesianClosedCategory
HereditarilyFinite.HF
HF_SetCat
HF_SetCat_Interp
HOL-Cardinals.Fun_More
HOL-Cardinals.Order_Relation_More
HOL-Cardinals.Wellfounded_More
HOL-Cardinals.Wellorder_Relation
HOL-Cardinals.Wellorder_Embedding
HOL-Cardinals.Order_Union
HOL-Cardinals.Wellorder_Constructions
HOL-Cardinals.Ordinal_Arithmetic
HOL-Cardinals.Cardinal_Order_Relation
HOL-Cardinals.Cardinal_Arithmetic
HOL-Cardinals.Wellorder_Extension
HOL-Cardinals.Cardinals
ZFC_in_HOL.ZFC_Library
ZFC_in_HOL.ZFC_in_HOL
ZFC_in_HOL.ZFC_Cardinals
ZFC_SetCat
ZFC_SetCat_Interp