Library HoTT.Categories.InitialTerminalCategory.Notations
Initial and terminal category notations
Require
InitialTerminalCategory.Functors
.
Require
InitialTerminalCategory.Pseudofunctors
.
Export
InitialTerminalCategory.Functors.InitialTerminalCategoryFunctorsNotations
.
Export
InitialTerminalCategory.Pseudofunctors.InitialTerminalCategoryPseudofunctorsNotations
.