Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
adding section on binary actions on identifications and the reference
Anonymous
added a little bit of whitespace to this equation, in order to make the syntax binding more evident to the eye:
$a \colon A \,, b\colon A \,, p \colon a =_A b \;\;\vdash\;\; \mathrm{ap}_f(a, b)(p) \,\colon\, f(a) =_B f(b)$This applies to other formulas, too, but I’ll leave it at that.
I have added more explicit pointers to section numbers in the references.
The current title (“action on identities”) of this entry seems bad: I don’t think “action” is a good word for “application”, but certainly “identities” is misleading. And that’s also not what the cited literature says (the cited literature says “paths” or “identifications”).
I vote for naming this entry “function application to identifications”.
Or if “action” must be in the title, then “action on identifications”.
Thanks!
So am taking the liberty then to also replace, in the title, the previous “identities” by “identifications”.
(An “identity” is either an identity morphism which here would be refl
, or else is a proposition asserting equality. In either case this is not what this entry is about.)
(An “identity” is either an identity morphism which here would be refl, or else is a proposition asserting equality. In either case this is not what this entry is about.)
And for that reason I don’t like the name “identity type”, since it implies that its terms are called “identities”, similar to how terms of function types are functions, and terms of natural number types are natural numbers.
I’d rather use “path type” or “identification type”. The word “identification” is used throughout the type theory literature but I have never seen “identification type” used in the type theory literature before. On the other hand, “path type” has been used in the literature, and makes sense as well since since every element of an identity type is given by a function from the interval type, but then in the context of cubical type theory one has to make the distinction between different notions of path type.
Very good. I am all for saying “Identification type”, as it’s clearly the right term: It is the data type of identification certificates.
And while we are at it, am for:
writing “$Id_{D}(d_1, \, d_2)$” instead of “$d_1 =_D d_2$”
as this is suggestive notation, avoids the weird clash with equality, and is still readable when the nesting level increases,
writing “$id_d$” instead of “$refl_d$” and call it the self-identification
I have added brief mentioning of the ($\infty$-)functoriality of $ap_f$ and added an illustrating graphics of the 0th and first stage: here
(This might want to go to a Properties-section, eventually, but given the structure of the entry at the moment, it seems most useful right here after the basic definition.)
My graphics uses somewhat different notational conventions than this (or other) entries. If this is found confusing and people insist, I can adjust this, but maybe I can alternatively nudge “us” into adopting this convention.
1 to 10 of 10