Many constructive theorem provers don't have native support for quotient types.
In order for presheafs over Set to work properly I need some sort of workaround.
Currently I'm using a simple approach of just adding in equivalence relations.
In pseudocoq
Record setoid := {
type:> Type ;
equal: type -> type -> Prop ;
setoid_Equivalence:> Equivalence equal
}.
A function is just a functor over setoids. I think this is called a Bishop set?
Record function A B := {
app: type A -> type B ;
map x y: x == y -> app x == app y
}.
Could a different style of things where a setoid is based around coequalizers work? Something like
Record setoid := {
type: Type ;
truncate: Type ;
p1: type -> truncate
p2: type -> truncate
}.
Definition equal (A: setoid) (x y: type A) := p1 x = p2 y.
The current approach is a bit painful sometimes and also I have worries about how constructive this approach is and if I'm suddenly going to wind up with a case I need excluded middle for. I took a quick look at apartness relations but they seemed even uglier.
Other stuff
A category is then something like
Record Category := {
object: Type ;
hom: object -> object -> setoid ;
id A: hom A A ;
compose A B C: hom B C -> hom A B -> hom A C
}.
Obeying the usual laws plus
map_compat A B: f == f' -> g == g' compose f g == compose f' g'
It gets a bit funky unfortunately which is why I'm looking at other approaches. I'm also not quite sure these is equivalent to the usual definition of enriched categories for the case of setoid.