Formalization of results from the literature

Content created by Fredrik Bakke, Vojtěch Štěpančík and Egbert Rijke.

Created on 2024-06-06.
Last modified on 2025-02-19.

This page is currently under construction. To see what’s happening behind the scenes, see the associated GitHub issue #1055.

Modules in the literature namespace

module literature where

open import literature.100-theorems public
open import literature.1000plus-theorems public
open import literature.idempotents-in-intensional-type-theory public
open import literature.introduction-to-homotopy-type-theory public
open import literature.oeis public
open import literature.sequential-colimits-in-homotopy-type-theory public

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.
[Rij22]
Egbert Rijke. Introduction to Homotopy Type Theory. 12 2022. arXiv:2212.11082.
[Shu17]
Michael Shulman. Idempotents in intensional type theory. Logical Methods in Computer Science, 12:1–24, 04 2017. arXiv:1507.03634, doi:10.2168/LMCS-12(3:9)2016.
[SvDR20]
Kristina Sojakova, Floris van Doorn, and Egbert Rijke. Sequential Colimits in Homotopy Type Theory. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, 845–858. Association for Computing Machinery, 07 2020. doi:10.1145/3373718.3394801.
[Wie]
Freek Wiedijk. Formalizing 100 theorems. URL: https://www.cs.ru.nl/~freek/100/.

Recent changes