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.
Your axioms combo might be fine, depending on what exactly you need; The Logic of Coq · coq/coq Wiki · GitHub has details. They don’t sound too constructive, but hopefully the result is constructive enough for your goals.
Your questions on “what can you get away with” seem hard to answer because requirements are likely missing — it seems you need to model in Coq some class of objects/
When formalizing specific setoid-respecting functions, we use quotients if we can define them (in specific cases), otherwise setoids. If you have a projection proj and functions f respecting the equality proj induces, you might define f on its codomain directly — but usually you can’t construct such a function from a relation, because quotients aren’t definable directly — but there are axioms for them you can add (not discussed in my link above).
Not sure what you mean, and I wouldn’t expect many in practice; Coq uses a universe hierarchy (so a bit more than ZFC) so talking of large categories resembles using Grothendieck universes; except that writing Type lets Coq infer (and check) the constraints on the needed universe.
I’m no expert, but if you want C_ex, wouldn’t it be a problem that setoids use equivalence relations while C_ex only pseudo-equivalence relations?
Precisely, we take the objects of C_ex to be the pseudo-equivalence relations in C […]
If (s,t):R→X×X is a monomorphism, then these conditions make it precisely a congruence or internal equivalence relation in C
1 Like
Your intuition is correct. The concept are related.
https://ncatlab.org/nlab/show/regular+and+exact+completions#TheExLexCompletion
The type theory corresponding to regular categories is the one using []-types, or truncations.
Mathematics and Computation | Propositions as [Types] (for extensional type theory)
or the hott book (or our paper on modalties) for the intensional story.
BTW the HoTT library works provides HITs and has an extensive cat th library, so you may want to have a look.
Yeah I’m mostly trying to understand the categorical semantics of some type theory stuff. I want it to be somewhat constructive so I can write some simple interpreters.
Yeah hopefully polymorphic universes minimises issues but what I mean is that I think it makes sense to construct “C0_ex” so to speak (I guess we’d think of this like Set?) from inside “C1” (I guess like Type). And I think it might make sense to construct “C1_ex” from inside “C2” and so on and so forth. But I would suspect in general you can’t construct completions from inside the universe you are working in. Even if you have polymorphic universes I suspect you’d still end up with weirdness. From a practical point of view I think polymorphic universes are certainly good enough for my purposes but I just want to get a better grip of the issues involved.
Because I’m working inside of Coq already I suspect I don’t have to make any special efforts to use internal setoids instead of external setoids. This stuff is weird because the category theory is describing the point of view from “outside” and I want to understand how to do things from “inside”.
Maybe but I’m still having trouble grasping the fine details of relating how things look from outside and inside. There are some finicky details involved. I think without extra axioms from outside Coq isn’t even a topos? Not sure about the metatheory here but my impression was things are a little bit messy/compromised for multiple uses?
My impression was that everything currently uses the private Inductive types hack. Also partly I’m attempting to do a little bit like HoTT but in my own words so I understand it.
Toposes are exact, so Coq is not a topos.
Indeed, the categorical semantics of Coq is not worked out very well.
Voevodsky’s notes on type systems was a start on that.
1 Like