search

agda / agda-categories

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

Add right adjoint to Functor.Slice.Forgetful #367

Closed Taneb closed 1 year ago

Taneb commented 1 year ago

Based on proposition 1.33 in Freyd's Aspects of Topoi

Taneb commented 1 year ago

I feel like both Forgetful and Free should have better names (especially as Free sometimes has a right adjoint of its own), but I don't know what they should be.

JacquesCarette commented 1 year ago

Nice. I have no suggestions as to a better name either. But maybe you should put the PR comment as a comment in the file too?