agda / agda-categories

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

Is Setoids its own exact completion? #282

Open JacquesCarette opened 3 years ago

JacquesCarette commented 3 years ago

See #281 for the construction. The question is then: is Setoids equivalent to its own exact completion? This is related to Michael Shulman's paper The derivator of Setoids.

Basically: in Set-based category theory, it isn't. But it E-Categories, it might be. There's all sorts of phenomena (see the paper, but also the discussion of it on the category theory Zulip) that are quite sensitive to whether it's Set-based or Setoid-based. That paper makes Setoids seem more and more 'inevitable' from some perspectives.