(** * Notations for categories *) Require Import Basics.Notations.Require Export Functor.Notations. Require Export NaturalTransformation.Notations. Require Export FunctorCategory.Notations. Require NatCategory. Export NatCategory.Notations. Require Export InitialTerminalCategory.Notations. Require Export Profunctor.Notations. Local Set Warnings "-notation-overridden". Require Export Comma.Notations. Require Export Adjoint.Notations. Require Export Structure.Notations. Require ChainCategory. Export ChainCategory.Notations.