From Categories Require Export Adjunction.Adjunction.
From Categories Require Export Adjunction.Duality.
From Categories Require Export Adjunction.Adj_Cat.
From Categories Require Export Adjunction.Adj_Facts.

