Hacker News Reader

Comment by igravious | Hacker News Reader

This link surfaced on HN before. :)

505 days ago to be precise during a discussion of the article “Relation Between Type Theory, Category Theory and Logic” on https://ncatlab.org/nlab/show/relation+between+type+theory+a...

Fascinating topic, previous discussion: https://news.ycombinator.com/item?id=9867465

View on HN

The second comment in the discussion is confusing. What's the significance of the order in the tuple? An unordered set should be enough, so the tuples would be obvious permutations. Is the order decoded in the elements, eg. the operator *?

Everything (written, anyway) contains an order.

The comment says that you may want to treat the same things in different orders as being the same "thing".

A better, in my opinion, English translation of the univalence axiom is, "identity is equivalent to equivalency" (formally, [(A=B)~(A~B)]). You can find this translation in the HoTT book[0].

Also, check out multisets[1].

[0] http://saunders.phil.cmu.edu/book/hott-online.pdf (PDF page 16, or book page 4)

[1] https://en.m.wikipedia.org/wiki/Multiset

You need to be able to write the group axioms down, so you need to distinguish the three elements. E.g. one of the axioms is 1 ∈ G, which means something very different from G ∈ 1. It all bottoms out in set theory, but (G, 1, X) really is a different set from (G, X, 1) (e.g. they might be represented as the sets {{G, 1, X}, {G, 1}, {G}} and {{G, 1, X}, {G, X}, {G}} respectively) so you do need to decide which is the "canonical" representation of that group, or else you need a rule that allows you to tell whether two different sets are representations of the same group.

Reply on news.ycombinator.com