(** * Adjunctions *)
(** ** Definitions *)
Require Adjoint.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(** *** unit+UMP *)
(** *** counit+UMP *)
(** *** unit+counit+zig+zag *)
Require Adjoint.UnitCounit.
(** *** universal morphisms *)
Require Adjoint.UniversalMorphisms.
(** *** hom-set isomorphism *)
Require Adjoint.Hom.
(** ** Coercions between various definitions *)
Require Adjoint.UnitCounitCoercions.
Require Adjoint.HomCoercions.
(** ** Opposite adjunctions *)
Require Adjoint.Dual.
(** ** Path spaces of adjunctions *)
Require Adjoint.Paths.
(** ** Composition *)
Require Adjoint.Composition.
(** ** Pointwise adjunctions *)
Require Adjoint.Pointwise.
(** ** Functoriality of any adjoint construction *)
Require Adjoint.Functorial.

Include Adjoint.Core.
Include Adjoint.UnitCounit.
Include Adjoint.UniversalMorphisms.Core.
Include Adjoint.Hom.
Include Adjoint.UnitCounitCoercions.
Include Adjoint.HomCoercions.
Include Adjoint.Dual.
Include Adjoint.Paths.
Include Adjoint.Composition.
Include Adjoint.Pointwise.
Include Adjoint.Functorial.Core.

Require Export Adjoint.Notations.