We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3456a23 commit 31133ddCopy full SHA for 31133dd
README.md
@@ -23,6 +23,11 @@ Documentation of the Lean code can be found
23
[here](https://sinhp.github.io/HoTTLean/docs/).
24
(We also have [a blueprint](https://sinhp.github.io/HoTTLean/),
25
but it is very outdated.)
26
+Relevant papers to this project are listed below
27
+- [A Certifying Proof Assistant for Synthetic
28
+Mathematics in Lean](https://voidma.in/assets/papers/2026nawrocki_certifying_proof_assistant_synthetic_mathematics_lean.pdf)
29
+- [Path Types in Algebraic Type Theory](https://arxiv.org/abs/2601.06567v1)
30
+- [Polynomial Functors in π-clans for the Semantics of Type Theory](https://arxiv.org/pdf/2602.05689)
31
32
### Dependencies
33
0 commit comments