Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMay 12th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexcreated _[[Homotopy Type System]]_ with an Idea-section

   created Homotopy Type System with an Idea-section

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeApr 17th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexfolded into two-level type theory <a href="https://ncatlab.org/nlab/revision/diff/Homotopy+Type+System/4">diff</a>, <a href="https://ncatlab.org/nlab/revision/Homotopy+Type+System/4">v4</a>, <a href="https://ncatlab.org/nlab/show/Homotopy+Type+System">current</a>

   folded into two-level type theory

   diff, v4, current

3. • CommentRowNumber3.
   • CommentAuthornLab edit announcer
   • CommentTimeJun 9th 2022
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexcopied article from HoTT Wiki Anonymous <a href="https://ncatlab.org/nlab/revision/diff/Homotopy+Type+System/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/Homotopy+Type+System/5">v5</a>, <a href="https://ncatlab.org/nlab/show/Homotopy+Type+System">current</a>

   copied article from HoTT Wiki

   Anonymous

   diff, v5, current

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeJul 14th 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRemoved claim that Voevodsky's conjecture implies model invariance. I don't know why I claimed that. <a href="https://ncatlab.org/nlab/revision/diff/Homotopy+Type+System/6">diff</a>, <a href="https://ncatlab.org/nlab/revision/Homotopy+Type+System/6">v6</a>, <a href="https://ncatlab.org/nlab/show/Homotopy+Type+System">current</a>

   Removed claim that Voevodsky’s conjecture implies model invariance. I don’t know why I claimed that.

   diff, v6, current

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 7th 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexadded pointer to: * [[Danil Annenkov]], [[Paolo Capriotti]], [[Nicolai Kraus]], [[Christian Sattler]]: *Two-Level Type Theory and Applications* &lbrack;[arXiv:1705.03307](https://arxiv.org/abs/1705.03307)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/Homotopy+Type+System/7">diff</a>, <a href="https://ncatlab.org/nlab/revision/Homotopy+Type+System/7">v7</a>, <a href="https://ncatlab.org/nlab/show/Homotopy+Type+System">current</a>

   added pointer to:

   • Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler: Two-Level Type Theory and Applications [arXiv:1705.03307]

   diff, v7, current