(** * Adjunctions *) Require Import Adjoint.UnitCounit. Require Import Basics.Notations. Notation Adjunction := AdjunctionUnitCounit. Module Export AdjointCoreNotations. Infix "-|" := Adjunction : type_scope. End AdjointCoreNotations.
(** * Adjunctions *) Require Import Adjoint.UnitCounit. Require Import Basics.Notations. Notation Adjunction := AdjunctionUnitCounit. Module Export AdjointCoreNotations. Infix "-|" := Adjunction : type_scope. End AdjointCoreNotations.