`adjunction_of_nat_iso_right`

b-mehta / topos

Topos theory in lean

56 stars 2 forks source link

Closed b-mehta closed 4 years ago

b-mehta commented 4 years ago

The dual of adjunction_of_nat_iso_left (in adjunctions.lean) and converse to #14

b-mehta commented 4 years ago

This was done by Thomas a while ago and should be in mathlib soon