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.
added to identity type a mentioning of the alternative definition in terms of inductive types (paths).
Thanks! It’s not really an alternative definition, though, just an encompassing of the other definition into a general framework. Also, it predates HoTT by a lot. I edited the page some trying to clarify.
Ah, okay. That wasn’t clear to me. Thanks.
I have added to identity type some discussion of the stability/coherence obstacles to interpreting identity types categorically in a WFS, along with some more references.
I added to identity type a discussion of how the definitional eta-conversion rule for identity types forces us into extensional type theory.
I wonder: is there a negative presentation of identity types?
at identity type in the section on categorical semantics I have added some actual details on how that proceeds. (to the existing discussion of what conditions on the ambient category we need for this.)
For fun, I have given identity type a lead-in quote
everything is identitcal with itself (WdL §863)
no two things are like each other (WdL §903)
Beyond being fun, it is reminiscent of how there is no way to prove equality than by reducing to reflection.
In a similar vein, I have been amused to notice that as Arthur grows up, one of the more difficult things for him to learn is that two things can be isomorphic without being identical (e.g. the beans on his plate and the beans on Dad’s plate).
You do realise that you and Urs now have the perfect opportunity to see how children brought up in the HoTT spirit will think mathematically.
Think how much harder at a later stage to work out how money works. Not only do they go through the stage of worrying about which particular coin they have, but that it’s treated as the same as combinations of coins.
David,
Even in my daily life, I’m often confronted with how plain bijections are not good isomorphisms in the category of coins, closed under addition. If it were, it would spare me some NP-complete problems.
Sure, everything I can buy with a 5er, I can also by with five 1’s. But if some machine takes two 1’s, I can’t use my 5er to get gum out of a machine. Its curious how money is partitioned into 1’s, 2’s, 5’s and 10-multiples of it. When I’m waiting in a cue, I always compute if I can generate all composites to pay “right”: With {1,2,2,5} you can pay 1,2,3,4,5,6,7,8,9. Funny how changing a 2 with a 1 only changes the upper bound, but not e.g your ability to produce 4. With more money, {1,5,5} say, you have far less options :) Having 11 units of money really isn’t just having 11 units of it. I was in Russia last month and when I ran out of money for some days, the boss of the firm we worked in said he’d help me out with some cash - of course I’d give him back whatever I didn’t need. Well, this guy then gave me a note worth a huge amount. I assume he meant the best, but to me it was an ass move as I just couldn’t break the note and give him back some small ones. He gave me too much and so he gave me nothing.
On my end, the Proceß has not expressed the moment of quantity yet, it still needs to sublate becoming into a more determinate being first. Also, I am still worried not so much about the identity type of beans as about it being inhabited at all.
Thanks David! This one was my fault, sorry, again it’s related to the unicode issues. When I get the time to try to fix things once and for all, I’ll look out for occurrences of this one.
As explained at the page eta-conversion, $\eta$-reduction, $\eta$-conversion, and $\eta$-expansion are technically all slightly different things, though of course very closely related. $\eta$-conversion is an undirected equivalence relation; $\eta$-reduction and $\eta$-expansion are the two opposite ways to “direct” this relation. Would it be useful to mention this point on the page identity type?
I wonder if we use these consistently, e.g., at Extensionality and η-conversion.
Hm, it seems that my first edit-message did not get through:
I had added pointer to Shulman 12 and was asking: Where is the origin of the observation that identity types are simply indctive type families generated by reflection?
Oh, way earlier than that. For instance, identity types are defined that way in Coq and have been since ever that I know of.
From say the inductive definition of identities types, it is clear that the interpretation of $Id_A(x,y)$ as the type of proofs that x is less than or equal to y is excluded?
For example, what if a type A is really an oo-category? So that $Id_A(x, y)$ is the type of morphisms from an object x of A to another object y of A. It would still be true that there is an identity morphism in $Id_A(x, x)$.
@Colin I think what you are trying to say is “can we have directed ’identitity’ types”. From the given inductive definition, the answer is a straight no however many people have and still are investigating similar types where they behave more like arrows of a category rather than of groupoids.
I wouldn’t call this the identitiy type however. The symmetry of Id_A(x,y) isn’t something we add on but it is actually something that can be proven so if you were to have an arrow type it wouldn’t look very similar to the identity type.
I would look at directed type theory, although I must say it isn’t very developed yet.
You can of course do category theory in HoTT, see sec 9.1 of the HoTT book. This will involve a type of objects and then a dependent type of morphisms between two objects. But that’s not the identity type. In a category, the type of isomorphisms between two objects will equal their identity type.
As Alizter says, also look at directed homotopy type theory.
There isn’t much content in the article David linked, but you should definitely look at some of the references. That is pretty much all the work that has been done on the topic.
Alizter, thank you very much for the pointers and for articulating what I was trying to ask in better language. Do you have a reference for a proof that $Id_A(x, y)$ is symmetric? Mike also makes a comment on the derivability of this at Martin-Löf+dependent+type+theory#equality_types.
Lemma 2.1.1 of the HoTT book. Essentially, by induction for identity types, you just have to show that the $refl$ terms have inverses, which clearly they do.
pointers to the original observations relating identity types to groupoids and higher groupoids were and still largely are missing from this entry. But I have now added at least these two:
Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (ed.) , Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). (ps)
Steve Awodey, Michael Warren, Homotopy theoretic models of identity type, Mathematical Proceedings of the Cambridge Philosophical Society vol 146, no. 1 (2009) (arXiv:0709.0248)
added ISBN and uploaded the pdf for:
This entry has offered no original references. I have now added pointer to
but that (that section 1.7) is hardly satisfactory. What’s a canonical original reference?
this one shows the rules, but gives no discussion otherwise:
This one has more:
added pointer to:
This article only focuses upon the identity types that appear in Martin-Löf type theory. So what do we do about all the other inequivalent identity types in other type theories, such as the identity types in cubical type theory defined using a primitive interval, and the identity types in higher observational type theory?
You need to ask what a reader deserves to see when looking for information and happening upon a page with a given title.
I suppose that a reader looking to understand what is meant by “identity type” will want to be shown all possible meanings. So if there are more than currently discussed in the page, then the page deserves to be re-organized/expanded.
started brief section on identity types in higher observational type theory, somebody with a better understanding of the subject like Mike Shulman could expand on it further
Anonymous
path type redirects here, but in the cubical type theory literature, path types are different from identity types in that most of them do not satisfy the J rule definitionally, but only up to a path.
created path type article. propositional equality redirects here as well, but should be created and made into a disambiguation article with links to both identity type and path type.
I would actually prefer that the phrase “identity type” be usable for whatever notion is appropriate for the particular type theory. This includes the Martin-Lof identity type (a.k.a. “jdentity type”), the path type of cubical type theroies, and the identity type of higher observational type theory, all of which satisfy different formal rules but are still “types of identifications”.
Andrew Swan thinks differently in this article
We give a collection of results regarding path types, identity types and univalent universes in certain models of type theory based on presheaves.
The main result is that path types cannot be used directly as identity types in any Orton-Pitts style model of univalent type theory with propositional truncation in presheaf assemblies over the first and second Kleene algebras.
We also give a Brouwerian counterexample showing that there is no constructive proof that there is an Orton-Pitts model of type theory in presheaves when the universe is based on a standard construction due to Hofmann and Streicher, and path types are identity types. A similar proof shows that path types are not identity types in internal presheaves in realizability toposes as long as a certain universe can be extended to a univalent one.
We show that one of our key lemmas has a purely syntactic variant in intensional type theory and use it to make some minor but curious observations on the behaviour of cofibrations in syntactic categories.
Yes, I’m aware that cubical type theorists tend to use “identity type” to mean the Martin-Lof one. (Although in cubical type theory there is also a “Swan identity type” that’s different from both path types and ML identity types.) I’m saying I would rather advocate a different usage. Some cubical type theorists have taken to calling the ML identity type the “jdentity type”, since its defining feature is the J rule.
As evidence supporting my preference, let me point out that the phrase “identity type” is already used in both intensional type theory and extensional type theory, even though the identity types of those two theories satisfy different rules.
Many cubical type theorists make the distinction between identity types like Martin-Löf’s identity types, Swan’s identity types, and the higher observational type theory identity types, where the rules for the identity types all imply the definitional J rule as a theorem (and they call all 3 types ’identity types’), vs the cubical path types where the rules only imply the J rule up to a path, and additional regularity rules are needed to make the J rule definitionally valid.
No additional regularity rule has been found to be compatible with univalence in cubical type theories yet.
Can we do better than this?
Identity types in cubical type theory are called path types and are defined using a primitive interval. I’m not exactly sure how they work so somebody with more expertise with cubical type theory should expand on it.
The identity types of higher observational type theory also do not satisfy definitional computation for J.
Also, if someone wants to do mathematics “agnostically” in higher type theory, so that what they write could be interpreted equally well in Book HoTT, cubical type theory, or higher observational type theory, they can do that technically by assuming just an “identity type” with a propositional J-rule. But they then have to call that type something, and I don’t know what they could call it other than an “identity type”.
@Guest at 43
Cubical type theorists make the distinction between path types and identity types because path types are literally functions out of an interval, just like how paths in Euclidean space are functions out of the unit interval, not because of the definitional/propositional J distinction. Otherwise, why are the types in XTT called “path types” instead of “identity types”? They satisfy definitional J by coercion and regularity.
Nathan
@Mike Shulman at 46
The definitional/propositional J could be distinguished by calling the identity type with definitional J a “strict identity type” and the identity type with propositional J a “weak identity type”. Type theory already uses “strict” and “weak” terminology for other such objects in type theory: compare “strict Tarski universe” vs “weak Tarski universe”, “strict proposition” and “weak proposition”, “strict squash type” and “weak squash type”, et cetera, where the difference between the structures are that the “strict” versions use definitional equality while the “weak” versions use propositional equality.
Nathan
Nathan,
If one includes the interval type in MLTT then identity types between objects of a type are also functions out of the interval to the type. But identity types in homotopy type theory (or any model of MLTT with the interval type) are not usually called “path types”. So that doesn’t explain why path types are called path types in cubical type theory.
The definitional J rule implies the propositional J rule, but the converse doesn’t hold, so one should take the propositional J rule to be the defining characteristic of identity types, as those apply for all known identity types, not just the Martin-Löf identity types. This is similar to the case for W-types and higher inductive types, the computation rules are only up to a path, rather than involving definitional equality.
The real problem with path types in cubical type theory are that technically they aren’t identity types, they are dependent identity types, in the same way a dependent function type is not a function type, and so they should actually be described on the article on dependent identity types rather than this article.
@50
What do you mean by “propositional J rule”?
Suppose one has a cubical higher observational type theory with Swan’s identity types; there are 3 separate identity types $\mathrm{idHOTT}$, $\mathrm{idSwan}$, and $\mathrm{Path}$. From there one could define 4 separate propositional computational rules (the elimination rule being the same for all 4) for the Martin-Löf identity types, resulting in 4 separate identity types $\mathrm{idML}0$, $\mathrm{idML}1$, $\mathrm{idML}2$, $\mathrm{idML}3$:
$\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}0_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idML}0_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)}$ $\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}1_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idHOTT}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)}$ $\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}2_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{idSwan}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)}$ $\frac{\Gamma \vdash a:A \quad \Gamma, x:A, p:\mathrm{idML}3_A(a, x) \vdash P(x, p) \; \mathrm{type}}{\Gamma, u:P(a, \mathrm{refl}_A) \vdash q:\mathrm{Path}_{P(a, \mathrm{refl}_A)}(\mathrm{indeq}_a(u, a, \mathrm{refl}_A), u)}$dependent path types in cubical type theory are not dependent identity types, because the interval primitive $I$ is not a type!
That is another reason why path types in cubical type theory should be considered different from identity types.
This discussion would be a lot easier to follow if everyone would sign their comments with a name. Pseudonyms would be fine, just something so we can distinguish between all the Guests and Anonymice. Please?!?
Re 48: I suppose, although I would prefer the meaning of “identity type” to be theory-dependent. In HOTT I wouldn’t want to have to always say “weak identity type” rather than just “identity type”.
Re 49: Not by definition. Book HoTT doesn’t have a notion of “extension type” that one could use to define a notion of “path type” out of the interval with fixed endpoints. So even though in some imprecise sense, identifications in Book HoTT are “equivalent to” functions out of the interval type, they’re not defined to be such the way they are in cubical type theories.
Re 51: The general form of path-types is a dependent identity type, but they specialize to non-dependent identity types in the case of constant dependence or reflexivity in the base. So they are identity types, and more. The identity types of HOTT also behave like this.
Re 52: But because any weak identity type is equivalent to any other, all of those propositional computation rules are inter-derivable. So the difference doesn’t really matter.
Re 54: What do you mean? The interval is not a type, but the path types are types!
There exist intensional type theories for which there is no such notion of definitional equality, and so the only possible notion of identification elimination in that theory is the one which uses the identity type for equality. Benno van den Berg and Martijn den Besten came up with such a type theory:
Although I’m not sure that this much detail about dependent identity types is appropriate in the “Idea” section. Maybe it should appear further down.
What does the semicolon mean in the judgment $J(t;x,y,p):C(x,y,p)$?
It’s just a way of separating the first argument of $J$ from the last three. Optional.
1 to 64 of 64