Not signed in (Sign In)

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

  • Sign in using OpenID

Discussion Tag Cloud

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
    • CommentTimeNov 2nd 2017

    started cubical type theory using a comment by Jonathan Sterling

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2017

    Which part of the entry is the quote?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2017

    everything below “quoting Jonathan Sterling”.

    I have pointed him to the entry, so that he can edit as need be.

    • CommentRowNumber4.
    • CommentAuthorjonsterling
    • CommentTimeNov 2nd 2017

    Thanks, Urs! I’ve made a minor clarification. Soon, I may add more to this page to reflect the work done by two groups here at CMU on cartesian versions of cubical type theory.

    • CommentRowNumber5.
    • CommentAuthorspitters
    • CommentTimeApr 24th 2018

    Adding references for HITs, canonicity.

    diff, v5, current

    • CommentRowNumber6.
    • CommentAuthorAlexisHazell
    • CommentTimeJan 4th 2019

    Added reference to “Parametric Cubical Type Theory” paper.

    diff, v6, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 4th 2019

    hyperlinked author names, and added arxiv: to before the arXiv identifiers

    diff, v7, current

    • CommentRowNumber8.
    • CommentAuthorspitters
    • CommentTimeFeb 6th 2019

    Recording the fact that Cartesian cubical sets are not equivalent to simplicial sets.

    diff, v8, current

    • CommentRowNumber9.
    • CommentAuthorspitters
    • CommentTimeFeb 15th 2019

    Adding Cavallo/Mortberg

    diff, v10, current

    • CommentRowNumber10.
    • CommentAuthorAli Caglayan
    • CommentTimeFeb 15th 2019

    @spitters This new one is still not equivalent to simplicial sets right?

    • CommentRowNumber11.
    • CommentAuthorspitters
    • CommentTimeApr 15th 2019

    Ref to: Homotopy canonicity for cubical type theory

    diff, v11, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeOct 8th 2019

    added pointer to

    diff, v13, current

  1. update references

    Evan Cavallo

    diff, v14, current

    • CommentRowNumber14.
    • CommentAuthorAlexisHazell
    • CommentTimeNov 20th 2019

    Added reference to Bentzen’s “Naive cubical type theory”.

    diff, v15, current

    • CommentRowNumber15.
    • CommentAuthorAlexisHazell
    • CommentTimeNov 20th 2019

    Fixed location of previous edit.

    diff, v15, current

  2. Updated dead link. from to

    Lasse Letager Hansen

    diff, v16, current

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJan 25th 2021

    Added some references to ABCFHL cartesian cubical type theory.

    diff, v18, current

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 29th 2021

    Added reference

    diff, v19, current

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 29th 2021

    Ah, ’normalization’ is a redirect for normal variety. This is misleading the link at sequent calculus too.

    What do people reckon is the best way to disambiguate?

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJan 29th 2021

    I don’t think there is ambiguity in disambiguation. Made a start here: normalization.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 29th 2021

    Thanks. I hadn’t seen we have appropriate other entries, such as normal form.

    • CommentRowNumber22.
    • CommentAuthorjonsterling
    • CommentTimeMay 3rd 2022

    Added my thesis to the normalization links

    diff, v21, current

    • CommentRowNumber23.
    • CommentAuthorGuest
    • CommentTimeAug 31st 2022

    cubical type theory is certainly not a “homotopy type theory in which univalence is not just an axiom but a theorem”. There exist extensional cubical type theories such as XTT where UIP is a theorem, not an axiom.

  3. edited first paragraph to explain that cubical type theories are not necessarily homotopy type theories, and added in a reference to the XTT paper as an example of a cubical type theory which is not a homotopy type theory.


    diff, v24, current

  4. adding reference


    diff, v25, current

  5. Fixed arXiv link in previous edit (s/abs:/abs\//) and pasted doi link from the arXiv page

    a distinct Anonymous

    diff, v27, current

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeSep 4th 2022

    Added some material that was at boundary (type theory)

    diff, v31, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeSep 21st 2022

    I have added to this entry missing cross-link to HoTT, by appending a half-sentence to the third paragraph (here).

    diff, v32, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)