search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Maybe the Hom version of Adjunction can be fully polymorphic? #351

Open JacquesCarette opened 2 years ago

JacquesCarette commented 2 years ago

See this discussion on twitter that points to this code on 1Lab that appears to do just that.

HuStmpHrrr commented 2 years ago

indeed this is the same as https://github.com/agda/agda-categories/blob/45798f85cde25c12dfff069a245ca9042c04b9b0/src/Categories/Adjoint.agda#L128-L130 if we unfold we don't need to match up universe levels.