Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** * Adjunctions *)
(** ** Definitions *)
Require Adjoint.Core.
(** *** 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.