Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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

    David, your link workshop points back to this thread…Is this intended ?

    • 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:22swap: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)(A), where AA 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.

    • CommentRowNumber14.
    • CommentAuthorGuest
    • CommentTimeAug 2nd 2022

    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.