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

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).

nLab > Latest Changes: cubical type theory

Bottom of Page

1 to 29 of 29

  1.  
    • 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

  13. 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

  16. Updated dead link. from http://www.cs.cmu.edu/~amoertbe/papers/cubicalagda.pdf to https://staff.math.su.se/anders.mortberg/papers/cubicalagda.pdf

    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.

  24. 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.

    Anonymous

    diff, v24, current

  25. adding reference

    Anonymous

    diff, v25, current

  26. 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

    • CommentRowNumber29.
    • CommentAuthorzuoke
    • CommentTimeSep 20th 2024
    Is "r=s:I" an typo?

1 to 29 of 29

  1.