This one has more:

- Per Martin-Löf, p. 31-34 in:
*Intuitionistic type theory*, Lecture notes Padua (notes by Giovanni Sambin), Bibliopolis, Napoli (1984) (pdf, MartinLofIntuitionisticTypeTheory.pdf:file)

this one shows the rules, but gives no discussion otherwise:

- Per Martin-Löf, p. 169 (17 of 23) in:
*Constructive Mathematics and Computer Programming*, Studies in Logic and the Foundations of Mathematics Volume 104, 1982, Pages 153-175 (doi:10.1016/S0049-237X(09)70189-2)

This entry has offered no original references. I have now added pointer to

- Per Martin-Löf, Section 1.7 in:
*An intuitionistic theory of types: predicative part*, in: H. E. Rose, J. C. Shepherdson (eds.),*Logic Colloquium ’73, Proceedings of the Logic Colloquium*, Studies in Logic and the Foundations of Mathematics**80**Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

but that (that section 1.7) is hardly satisfactory. What’s a canonical original reference?

]]>added ISBN and uploaded the pdf for:

- Martin Hofmann, Thomas Streicher
*The groupoid interpretation of type theory*, in: Giovanni Sambin et al. (eds.) ,*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). (ISBN:9780198501275, ps, pdf)

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)

Fixed a tiny typo: an -> a

anqurvanillapy

]]>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.

]]>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.

]]>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.

]]>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.

]]>@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.

]]>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)$.

]]>Oh, way earlier than that. For instance, identity types are defined that way in Coq and have been since ever that I know of.

]]>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?

]]>also pointer to Licata 11. Is that where the observation originates?

]]>I wonder if we use these consistently, e.g., at Extensionality and η-conversion.

]]>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?

]]>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.

]]>Some of the βs and ηs had become $\infty$ in links, so I fixed this.

I guess we just live with using η-reduction, -conversion, -expansion interchangeably.

]]>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.

]]>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.

]]>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.

]]>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).

]]>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.

]]>