Ну и что тут непонятного, если вы проходили мой курс по ФП на F# ?
(а тем более, если трек по HoTT :)

Это малышовый пример по монадам со Стэнфордского курса
"CS 99: Functional Programming and Theorem Proving in Lean 4"

Вот что примерно будем делать (похищаю смыслы:) =>

The course project involves formalizing a non-trivial piece of mathematics or computer science in Lean 4.
(Easy) Formalize a solution to a (at least undergraduate level) textbook math or CS problem
(Medium) Formalize a board game that has not been done before. e.g. chess. The formalization should be at a level where it is possible to prove winning conditions.
(Medium) Formalize program verification primitives
(Medium) Formalize natural languages
(Hard) Contribute to Mathlib4 or other Lean formalization libraries
(Hard) Fix a Lean bug

Скоро будете у меня круче Гарварда-Стэнфорда :)

Техлиды, заглянув в ваш гитхаб, будут шептать "что ты такое??" :)