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 canonical form references (talk notes) on canonicity or not in the presence of univalence
With my workshop happening, I seem to keep hearing about the delights of canonicity. Coming from the category theoretic side, what’s the deal with it?
Do I understand from this in the HoTT book
This construction of the free monoid is possible essentially because elements of the free monoid have computable canonical forms (namely, finite lists). However, elements of other free (and presented) algebraic structures — such as groups — do not in general have computable canonical forms. For instance, equality of words in group presentations is algorithmically undecidable. However, we can still describe free algebraic objects as higher inductive types, by simply asserting all the axiomatic equations as path constructors.
that canonicity goes as soon as we do any non-trivial algebra. So why should I care?
Two specific questions:
Is it that as soon as we have HITs with a path constructor that we lose canonicity?
In the example on canonical form where it shows how a use of univalence gets stuck, was the function from to itself chosen just as an example of a non-identity isomorphism?
David, your link workshop points back to this thread…Is this intended ?
Thanks! Fixed now.
canonicity goes as soon as we do any non-trivial algebra
Well, most nontrivial algebraic structures, like groups, rings, and so on are defined the way they are for other (perfectly good) reasons, and not with canonicity or computation in mind. So it’s not surprising that free algebras don’t have canonical forms. But when we view type theory as an “algebraic theory” of sorts, then it is usually constructed so as to be “computable” and therefore to have canonical forms, even though it is of course highly nontrivial (and the proof that it does have canonical forms is likewise highly nontrivial).
Is it that as soon as we have HITs with a path constructor that we lose canonicity?
The way HITs are currently defined in “Book HoTT” as well as in Coq, Agda, and Lean, yes. Cubical type theory can handle at least some HITs while retaining canonicity.
In the example on canonical form where it shows how a use of univalence gets stuck, was the function from to itself chosen just as an example of a non-identity isomorphism?
Yes. I don’t know why that example was chosen; there are much simpler nonidentity isomorphisms like .
Thanks!
Cubical type theory can handle at least some HITs while retaining canonicity.
What of is_inhab, where has canonical elements?
You mean the propositional truncation? Yes, that’s one of the ones they do.
Yes, great. Where do they do this? Who are ’they’ anyway?
One “they” is Thierry Coquand and his coauthors: the propositional truncation is on p20 of this paper. Dan Licata and Guillaume Brunerie were independently working on a cubical type theory for at least a while, but I don’t think they’ve actually posted a writeup yet; the slides available on Dan’s web site don’t mention the truncation. The recent Angiuli-Harper-Wilson paper also doesn’t mention truncation explicitly. But I’m sure that it will work just about as well in all versions.
Thanks. It’s p.25 of the Coquand et al. paper if anyone’s looking.
Despite having heard various talks about it, I keep being uncertain as to what the claim regarding cubical type theory and univalence really is. It sounds as if the following is claimed: “In principle it is possible to take any proof in book HoTT that uses univalence and systemaically turn it into a program that computes.” Has this been proven?
I’m not the best person to answer that, since I have trouble keeping up with all the different cubical theories and exactly what has and hasn’t been done (and I have to admit that keeping up with all of them is not high on my priority list). That’s certainly the goal (although “program that computes” has to be taken with a grain of salt — only a term belonging to a type like nat or bool will actually compute a “value” in the ordinary sense), and a lot of progress has been made. But there have been various technical issues that I don’t know whether have all been dealt with at once, regarding things like whether the rules for paths in the universe (univalence) can be consistently defined at all levels, and whether Id-elim satisfies its computation rule judgmentally or only typally.
One such result is here it also refers to a proof of canonicity for by the cubical team, which hopefully will be published shortly.
Higher inductive types also break canonicity if the identity types used in defining higher inductive types are Martin-Löf’s identity types. I don’t see this fact stated anywhere in the article.
1 to 16 of 16