Closed andrejbauer closed 11 years ago
I vote for continuing to use the standard identity type. (Why have we defined our own 'inverse'?)
On Sun, Dec 16, 2012 at 11:45 PM, Andrej Bauer notifications@github.comwrote:
We have now defined our own concat and inverse in Paths.v, even though the equivalent identity_trans and identity_sym exist in the standard library. Would it make sense to just go all independent and define our own identity type? And call it paths? I think the ssreflect library won't be too happy about that.
— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/HoTT/issues/35.
We're using our own identity type now, defined as paths
in Overture.v
. I think there was some discussion of this offline that led to that decision; do you remember what it was? The reasoning should perhaps be recorded somewhere.
We wanted more control over transitivity, symmetry and inverse. But we were not allowed to change those for the standard eq/identity type (or its Type-valued version) because it broke various other standard things. And we were not allowed to rename anything, so we used notations, which sort of worked except it did not quite work, etc.
Okay, I added a comment to this effect in Overture.v where we define our identity type.
We have now defined our own
concat
andinverse
inPaths.v
, even though the equivalentidentity_trans
andidentity_sym
exist in the standard library. Would it make sense to just go all independent and define our own identity type? And call itpaths
? I think the ssreflect library won't be too happy about that.