Author: nLab edit announcer Format: MarkdownItexAdding reference to
A Syntax for Higher Inductive-Inductive Types
Ambrus Kaposi and András Kovács
Bas Spitters
<a href="https://ncatlab.org/nlab/revision/diff/inductive-inductive+type/9">diff</a>, <a href="https://ncatlab.org/nlab/revision/inductive-inductive+type/9">v9</a>, <a href="https://ncatlab.org/nlab/show/inductive-inductive+type">current</a>
Adding reference to
A Syntax for Higher Inductive-Inductive Types
Ambrus Kaposi and András Kovács
Author: nLab edit announcer Format: MarkdownItexThe link (https://akaposi.github.io/hiit.pdf) for Ambrus Kaposi and András Kovács, _A Syntax for Higher Inductive-Inductive Types_ was out of date (404 on Sept 5, 2018), and Ambrus Kaposi's website (https://akaposi.github.io) now links to the inserted page.
Jasper Hugunin
<a href="https://ncatlab.org/nlab/revision/diff/inductive-inductive+type/11">diff</a>, <a href="https://ncatlab.org/nlab/revision/inductive-inductive+type/11">v11</a>, <a href="https://ncatlab.org/nlab/show/inductive-inductive+type">current</a>
The link (https://akaposi.github.io/hiit.pdf) for Ambrus Kaposi and András Kovács, A Syntax for Higher Inductive-Inductive Types was out of date (404 on Sept 5, 2018), and Ambrus Kaposi’s website (https://akaposi.github.io) now links to the inserted page.
Author: spitters Format: MarkdownItexWork by Jasper Hugunin reducing IndInd to Ind in CTT.
<a href="https://ncatlab.org/nlab/revision/diff/inductive-inductive+type/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/inductive-inductive+type/14">v14</a>, <a href="https://ncatlab.org/nlab/show/inductive-inductive+type">current</a>
Work by Jasper Hugunin reducing IndInd to Ind in CTT.
Author: nLab edit announcer Format: MarkdownItexadded example of a univalent Tarski universe as a higher inductive-inductive type
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/inductive-inductive+type/16">diff</a>, <a href="https://ncatlab.org/nlab/revision/inductive-inductive+type/16">v16</a>, <a href="https://ncatlab.org/nlab/show/inductive-inductive+type">current</a>
added example of a univalent Tarski universe as a higher inductive-inductive type
Author: Urs Format: MarkdownItexboosted the list of references a little
<a href="https://ncatlab.org/nlab/revision/diff/inductive-inductive+type/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/inductive-inductive+type/17">v17</a>, <a href="https://ncatlab.org/nlab/show/inductive-inductive+type">current</a>