Timeline for Question about higher inductive types and computational rules
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 13, 2014 at 15:08 | comment | added | Mike Shulman | @FrançoisG.Dorais, my answers were based on what I took the question to be from reading his reply to my first comment. Your reading sounds more like what he wrote in the original question, but I wasn't able to understand exactly what he was asking there. | |
| Aug 7, 2014 at 23:15 | comment | added | François G. Dorais | My reading of the question seems to be a bit different from Mike's. I think Gabriel wants to avoid postulating identity constructors and replace them by "indistinguishability rules", i.e. what would result from substitution but without assuming that the terms are "equal" (it's unclear to me whether Gabriel means for "equal" to be propositional or definitional). I'm not sure but my hunch is that these rules could be powerful enough to recover the identity rules in the propositional sense but not in the definitional sense. | |
| Aug 7, 2014 at 16:35 | answer | added | Mike Shulman | timeline score: 1 | |
| Aug 7, 2014 at 16:31 | answer | added | Mike Shulman | timeline score: 5 | |
| Aug 7, 2014 at 5:48 | comment | added | Gabriel | Thanks. In the meantime, I reread a couple of pages on equality and identity proofs, etc. on ncatlab, and it made it somewhat clearer for me. Although, it's still confusing to me why in some cases we'd want to encode our more fundamental relations like udn=n as propositional equalities and in other cases as definitional ones, but I guess continuing reading about the subject will eventually blow away the fog. | |
| Aug 7, 2014 at 3:06 | comment | added | Mike Shulman | Ah, I think I see. I will try to answer. | |
| Aug 6, 2014 at 22:02 | comment | added | Gabriel | Sorry if this is unclear, it's all very new to me. I guess I'm just confused as to why identity proof constructors would be necessary. The reason why he added the constructor for the type u(d(n))=n, was so that he could say that going up and then down was the same as not moving. But aren't computation rules there exactly for this kind of question? Why didn't he just define instead a computation rule udn=n : Z? If he later wanted to use the type udn=n, he would have had it with "ref", since the computation says that they're "the same". Maybe there is a reason why having a term udn=n is bad? | |
| Aug 6, 2014 at 19:24 | comment | added | Mike Shulman | I don't understand what you're proposing; can you write it out in more detail? | |
| Aug 5, 2014 at 5:42 | history | edited | Gabriel |
edited tags
|
|
| Aug 5, 2014 at 5:39 | review | First posts | |||
| Aug 5, 2014 at 7:22 | |||||
| Aug 5, 2014 at 5:36 | history | asked | Gabriel | CC BY-SA 3.0 |