(** * Initial and terminal category notations *)Require InitialTerminalCategory.Pseudofunctors. Export InitialTerminalCategory.Functors.InitialTerminalCategoryFunctorsNotations. Export InitialTerminalCategory.Pseudofunctors.InitialTerminalCategoryPseudofunctorsNotations.