Library HoTT.Categories.Adjoint.Core

Adjunctions

Require Import Adjoint.UnitCounit.
Require Import Basics.Notations.

Notation Adjunction := AdjunctionUnitCounit.

Module Export AdjointCoreNotations.
  Infix "-|" := Adjunction : type_scope.
End AdjointCoreNotations.