Adjunctions, Limits, and Colimits in Univalent Categories

Opening obstruction

Univalence identifies equivalent objects, but ordinary categorical constructions must still be rebuilt so their universal properties respect that identity.

Development contract

Develop adjunctions, limits, colimits, and representability in univalent categories, proving invariance and uniqueness results rather than importing ordinary-category slogans.