I’ve been working with a little bit of constructive category theory but because higher inductive types are far from ready I need to work with setoids. In my case I need to use a constructive approach because I hope to work on some type theory/compiler stuff.

I read up on the categorical side of things and I think setoids kind of correspond to a free completion.

https://ncatlab.org/nlab/show/regular+and+exact+completions#the_higher_categorical_approach

I am pretty sure C_ex corresponds to setoids.

I think C_reg can be interpreted as equipping types with a projection and defining equivalence off of that but things might be more subtle.

```
Class Truncate A := {
codomain: Type ;
proj: A -> codomain ;
}.
Instance A `(Truncate A): Setoid A := {
equiv x y := truncate x = truncate y ;
}.
```

Identity is easier to work with than equivalence but I’m not quite sure of how to work with the second approach or some of the categorical semantics of Coq.

I don’t quite understand if or how I could get by with C_reg rather than C_ex.

I’m not quite certain but I think at least some sort of predicate extensionality is required for C_ex to work (you could truncate a function to a relation and compare those) but I’m not quite sure how predicate extensionality interacts with other axioms like excluded middle.

- Am I generally correct about what the completions correspond to modulo universe issues?
- Can I get away with C_reg instead of C_ex? Do I need predicate extensionality for this?
- I don’t understand the universe issues involved.
- I don’t understand axioms required to make these approaches work.
- Any alternative approaches I’m missing out on? For example I’ve been thinking about defining equivalence as the propositional truncation of an isomorphism.