Timeline for Are all group monomorphisms regular, constructively?
Current License: CC BY-SA 2.5
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 22, 2012 at 23:45 | comment | added | David Roberts♦ | "Monic win"? That's the worst joke I've seen in ages :) | |
| Oct 8, 2010 at 19:04 | history | edited | Monic Win | CC BY-SA 2.5 |
add correction and explanation
|
| Oct 8, 2010 at 4:19 | comment | added | Andrej Bauer | And I might write a blog post. It's interesting to have a non-contrived constructive result which fails in PERs. | |
| Oct 7, 2010 at 21:07 | comment | added | Monic Win | Well, that's okay, since I actually meant for the answer in PER to translate to CZF :-) :-) Unless I've made some other mistake (like if Markov's Principle is hiding somewhere) then the original question is answered, and the critical insight is in fact due to you. Of course now I'm quite surprised to hear that it wouldn't work the other way. So yes, I will have to look at your thesis. | |
| Oct 7, 2010 at 20:40 | comment | added | Andrej Bauer | In CZF quotients are as they're supposed to be. They're generated with collection, I suppose? But beware, CZF is not the internal language of PERs and you can't just conclude that anything holding in CZF is valid in PERs. And no, we are not talking about things being c.e., we're talking about the interpretation of first-order logic in the category of PERs. Have a look at my Ph.D thesis. | |
| Oct 7, 2010 at 20:29 | comment | added | Monic Win | Incidentally CZF is predicative. There are exponentials but no powersets (no subobject classifier). So I hope there is no need to go to toposes. | |
| Oct 7, 2010 at 20:26 | comment | added | Monic Win | Is that right? I thought $\left|x\right| = \left|y\right|$ means exactly $R^{\ast}(x,y)$. Multiplication has to be compatible with $R^{\ast}$, but otherwise it just acts on the underlying $G^{\ast} \subset \mathbb{N}$. Notice that in my definition of PER I have not required the complement of $R$ to be c.e. either, perhaps that is what you are thinking? | |
| Oct 7, 2010 at 16:32 | comment | added | Andrej Bauer | Your answer has a problem, at least in PERs, namely, because the "appropriate equivalence relation", call it $\sim$, is not $\lnot\lnot$-stable there is going to be a hole in your reasoning at some point: you will want to conclude $x \sim y$ from $[x] = [y]$, but that won't be possible. Nevertheless, I think your construction works in a setting in which equivalence relations are effective (a topos, for example). | |
| Oct 7, 2010 at 16:30 | comment | added | Andrej Bauer | Equality in the category of PERs is stable, I am very sure of this. Your existence of a rewrite path, for example, is external and not internal. Let me put this another way. Suppose we have an equivalence relation $\sim$ on a per $A$, i.e., a mono ${\sim} \to A \times A$ which is an equivalence relation. The quotient per $A/{\sim}$ satisfies in the internal language $$\lnot\lnot (x \sim y) \iff [x] = [y]$$ where $[{-}] : A \to A/{\sim}$ is the canonical quotient. Another way to say this is that quotients in PER are not effective. | |
| Oct 7, 2010 at 14:13 | history | answered | Monic Win | CC BY-SA 2.5 |