Library HoTT.Categories.Adjoint.Functorial

Functoriality of the construction of adjunctions

Computational components

Require Adjoint.Functorial.Parts.

Functor laws

Require Adjoint.Functorial.Laws.

Adjunction functor

Require Adjoint.Functorial.Core.