WorkAdventure/library.html

<html>
    <head>
        <style type="text/css">
         a { color: #0366d6; text-decoration: none; }
         a :hover { text-decoration: underline; }
         a :visited { color: #0366d6; text-decoration: none; }
        </style>
    </head>
    <body>
        <h1 id="links-for-a-hott-library">Links for a HoTT Library</h1>
        <h2 id="general-links-">General links:</h2>
        <ul>
            <li><a href="https://hott.github.io/book/nightly/hott-online-1287-g1ac9408.pdf">The HoTT book</a></li>
            <li>Egbert Rijke&#39;s book — on Discord, no public link?</li>
        </ul>
        <h2 id="day-1-introduction-to-hott-">Day 1 – Introduction to HoTT:</h2>
        <ul>
            <li><a href="https://raw.githubusercontent.com/UniMath/Schools/master/2019-04-Birmingham/Part1_Spartan_Type_Theory/Spartan-Type-Theory.pdf">Spartan MLTT</a></li>
            <li><a href="https://github.com/andrejbauer/homotopy-type-theory-course#homotopy-type-theory">Andrej Bauer&#39;s course in Ljubjana</a></li>
        </ul>
        <h2 id="day-2-the-coq-hott-library-">Day 2 – The Coq-HoTT Library:</h2>
        <ul>
            <li><a href="https://coq.inria.fr/refman/">Coq&#39;s reference manual</a></li>
            <li><a href="http://hott.github.io/HoTT/proviola-html/toc.html">The library&#39;s reference manual</a></li>
            <li><a href="http://hott.github.io/HoTT/proviola-html/HoTTBook.html">Correspondance between the library and the HoTT book</a></li>
        </ul>
        <h2 id="day-3-models-of-hott-">Day 3 — Models of HoTT:</h2>
        <ul>
            <li><a href="https://arxiv.org/abs/1611.02108">Cubical Type Theory: a constructive interpretation of the univalence axiom</a></li>
            <li><a href="https://arxiv.org/abs/1802.01170">On Higher Inductive Types in Cubical Type Theory</a></li>
        </ul>
        <h2 id="day-4-cubical-agda-">Day 4 – Cubical Agda:</h2>
        <ul>
            <li><a href="https://vimeo.com/459020971">Every proof assistant: Cubical Agda</a></li>
            <li><a href="https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf">Cubical Agda: A Dependently TypedProgramming Language with Univalence andHigher Inductive Types</a></li>
            <li><a href="https://arxiv.org/abs/2009.05547">Internalizing Representation Independence with Univalence</a></li>
            <li><p><a href="https://staff.math.su.se/anders.mortberg/papers/cubicalmethods.pdf">Lecture Notes of the 2019 HoTT Summer School</a></p>
            </li>
            <li><p><a href="https://github.com/agda/cubical/blob/master/Cubical/README.agda">Quick overview of the library</a></p>
            </li>
            <li><a href="https://agda.readthedocs.io/en/v2.6.1.3/">Agda&#39;s user manual</a></li>
        </ul>
        <h2 id="day-5-synthetic-hott-">Day 5 — Synthetic HoTT:</h2>
    </body>
</html>