# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeSep 4th 2012

added to canonical form references (talk notes) on canonicity or not in the presence of univalence

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeMay 5th 2016
• (edited May 5th 2016)

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 $\mathbb{N}$ to itself chosen just as an example of a non-identity isomorphism?

• CommentRowNumber3.
• CommentAuthorzskoda
• CommentTimeMay 5th 2016

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeMay 5th 2016

Thanks! Fixed now.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeMay 5th 2016

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 $\mathbb{N}$ 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 $swap:2\to 2$.

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeMay 5th 2016
• (edited May 5th 2016)

Thanks!

Cubical type theory can handle at least some HITs while retaining canonicity.

What of is_inhab$(A)$, where $A$ has canonical elements?

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeMay 5th 2016

You mean the propositional truncation? Yes, that’s one of the ones they do.

• CommentRowNumber8.
• CommentAuthorDavid_Corfield
• CommentTimeMay 5th 2016

Yes, great. Where do they do this? Who are ’they’ anyway?

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeMay 5th 2016

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.

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeMay 6th 2016

Thanks. It’s p.25 of the Coquand et al. paper if anyone’s looking.

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMay 6th 2016

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?

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeMay 6th 2016

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.

• CommentRowNumber13.
• CommentAuthorspitters
• CommentTimeMay 14th 2016

One such result is here it also refers to a proof of canonicity for by the cubical team, which hopefully will be published shortly.