Library HoTT.Categories.Adjoint.Core
Require Import Adjoint.UnitCounit.
Require Import Basics.Notations.
Notation Adjunction := AdjunctionUnitCounit.
Module Export AdjointCoreNotations.
Infix "-|" := Adjunction : type_scope.
End AdjointCoreNotations.
Require Import Basics.Notations.
Notation Adjunction := AdjunctionUnitCounit.
Module Export AdjointCoreNotations.
Infix "-|" := Adjunction : type_scope.
End AdjointCoreNotations.