agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard
verified publisher icon agda

More general preservation of limits

Open JacquesCarette opened this issue 5 years ago • 0 comments

As was mentioned in https://github.com/agda/agda-categories/pull/191#discussion_r475220761

in case one wants a more general preservation of limits, we can get that from the fact that strong equivalence induces adjointness, and then we can apply RAPL to get that property.

JacquesCarette avatar Jan 01 '21 22:01 JacquesCarette