Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Small docs fixes/improvement #178

Merged
merged 2 commits into from
Apr 4, 2024
Merged

Small docs fixes/improvement #178

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fd803de
Fix Markdown formatting in the changelog
fizruk Apr 4, 2024
0aae3bf
Mention Ground Zero project (HoTT formalization in Lean 4)
fizruk Apr 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Mention Ground Zero project (HoTT formalization in Lean 4)
  • Loading branch information
@fizruk
fizruk committed Apr 4, 2024
commit 0aae3bf93a4174ca7caace7b8c8f7f90a1e380e1
20 changes: 11 additions & 9 deletions docs/docs/en/related.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,13 +39,13 @@ Aya is implemented in Java.

I do not know of existing formalization libraries in Aya.

## The <b><span style="color: red">red</span>*</b> family
## The <b><span style="color: red">red</span>\*</b> family

[<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt), [<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt), and [<b><span style="color: red">Red</span>PRL</b>](https://redprl.readthedocs.io/en/latest/) are a family of experimental proof assistants developed by the [<b><span style="color: red">Red</span>PRL</b> Development Team](https://redprl.org).

There is a [<b><span style="color: red">red</span>tt</b> mathematical library](https://github.com/RedPRL/redtt/tree/master/library)

The <b><span style="color: red">red</span>*</b> family of proof assistants is implemented in OCaml.
The <b><span style="color: red">red</span>\*</b> family of proof assistants is implemented in OCaml.
The developers also have a related [<b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b> project](https://redprl.org/#algae),
which aims to provide composable (OCaml) libraries that facilitate the construction of a usable proof assistant from a core type checker.

Expand All @@ -60,6 +60,7 @@ Other notable formalizations of HoTT in Coq include [Coq-HoTT](https://github.co
Coq is implemented in OCaml.

## Cubical Agda

[Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) is a mode extending Agda with a variety of features from Cubical Type Theory[^1] [^2].

Although technical a mode within Agda, it is probably best seen as a separate language.
Expand Down Expand Up @@ -89,7 +90,11 @@ Hence, a formalization of [HoTT in Lean 2](https://github.com/leanprover/lean2/t
However, since Lean 2 is not supported anymore, the formalization is also unmantained.

Lean 3 and 4 has dropped the mode that allowed (direct) HoTT formalization.
There is, however, an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3).
However, the [Ground Zero](https://github.com/forked-from-1kasper/ground_zero) project
attempts to formalize HoTT in Lean 4. The project makes use of the [large elimination checker](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
ported from an unmaintained [port of Lean 2 HoTT Library to Lean 3](https://github.com/gebner/hott3),
which enables HoTT and non-HoTT scopes to coexist consistently (as the project authors believe).
In particular, attempting to show UIP results in a type error under HoTT scope in the Ground Zero project.

Lean 2 and 3 are implemented in C++.
Lean 4 is implemented in itself (and a bit of C++)!
Expand All @@ -102,22 +107,19 @@ Lean 4 is implemented in itself (and a bit of C++)!
<https://doi.org/10.4230/LIPIcs.TYPES.2015.5>

[^2]:
Thierry Coquand, Simon Huber, and Anders Mörtberg.
2018. _On Higher Inductive Types in Cubical Type Theory_.
Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
Association for Computing Machinery, New York, NY, USA, 255–264.
<https://doi.org/10.1145/3209108.3209197>

[^3]:
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
Association for Computing Machinery, New York, NY, USA, 164–172.
<https://doi.org/10.1145/3018610.3018615>

[^4]:
Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
2017. _Homotopy Type Theory in Lean_.
Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
<https://doi.org/10.1007/978-3-319-66107-0_30>
23 changes: 13 additions & 10 deletions docs/docs/ru/related.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ Aya реализована на Java.

Мне неизвестны библиотеки формализации на Aya.

## Семейство <b><span style="color: red">red</span>*</b>
## Семейство <b><span style="color: red">red</span>\*</b>

[<b><span style="color: #135cb7;">cool</span>tt</b>](https://github.com/redprl/cooltt),
[<b><span style="color: red">red</span>tt</b>](https://github.com/redprl/redtt),
Expand All @@ -54,8 +54,8 @@ Aya реализована на Java.

Существует формализация [математической библиотеки <b><span style="color: red">red</span>tt</b>](https://github.com/RedPRL/redtt/tree/master/library)

Семейство решателей <b><span style="color: red">red</span>*</b> реализовано на языке программирования OCaml.
Создатели семества решателей также работают над [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
Семейство решателей <b><span style="color: red">red</span>\*</b> реализовано на языке программирования OCaml.
Создатели семества решателей также работают над [проектом <b><span style="color: rgb(133, 177, 96);">A.L.G.A.E.<span></b>](https://redprl.org/#algae),
который нацелен на реализацию ряда удобных библиотек (для OCaml) для помощи в реализации
решателей теорем на основе проверки типов для ядра решателя.

Expand All @@ -70,6 +70,7 @@ Coq — это зрелый решатель теорем, основанный
Coq реализован на OCaml.

## Cubical Agda

[Cubical Agda](https://agda.readthedocs.io/en/latest/language/cubical.html) (кубическая Агда)
— это расширение Agda набором возможностей кубической теории типов[^1] [^2].

Expand Down Expand Up @@ -102,7 +103,12 @@ Lean 2, как и Agda, поддерживал режим без уникаль
Однако, Lean 2 больше не поддерживается и формализация, соответственно, тоже.

Lean 3 и 4 убрали режим, допускающий (прямую) формализацию гомотопической теории типов.
Однако, существует ныне неподдерживаемый [проект по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
Несмотря на это проект [Ground Zero](https://github.com/forked-from-1kasper/ground_zero)
продолжает формализацию HoTT на Lean 4. Проект использует [проверку элиминации](https://github.com/forked-from-1kasper/ground_zero/blob/d8c41ea2910d81d3c1bf6c2762663473368016ab/GroundZero/Meta/HottTheory.lean),
портированную из неподдерживаемого [проекта по переносу библиотеки HoTT с Lean 2 на Lean 3](https://github.com/gebner/hott3).
Эта проверка позволяет поддерживать окружение HoTT, совместимое со стандартным окружением Lean (по крайней мере по убеждениям авторов проекта).
В частности, попытка (напрямую) доказать принцип неразличимости доказательств равенства (Uniqueness of Identity Proofs)
приводит к ошибки типизации в рамках проекта Ground Zero.

Lean 2 и 3 реализованы на C++.
Lean 4 реализован в основном на самом себе (и немного на C++)!
Expand All @@ -115,22 +121,19 @@ Lean 4 реализован в основном на самом себе (и н
<https://doi.org/10.4230/LIPIcs.TYPES.2015.5>

[^2]:
Thierry Coquand, Simon Huber, and Anders Mörtberg.
2018. _On Higher Inductive Types in Cubical Type Theory_.
Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. _On Higher Inductive Types in Cubical Type Theory_.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18).
Association for Computing Machinery, New York, NY, USA, 255–264.
<https://doi.org/10.1145/3209108.3209197>

[^3]:
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. _The HoTT library: a formalization of homotopy type theory in Coq_.
In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017).
Association for Computing Machinery, New York, NY, USA, 164–172.
<https://doi.org/10.1145/3018610.3018615>

[^4]:
Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz.
2017. _Homotopy Type Theory in Lean_.
Floris van Doorn, Jakob von Raumer & Ulrik Buchholtz. 2017. _Homotopy Type Theory in Lean_.
In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017.
Lecture Notes in Computer Science(), vol 10499. Springer, Cham.
<https://doi.org/10.1007/978-3-319-66107-0_30>
Loading