у меня просто есть подозрение что без тоталити чекинга в какой-то форме осмысленно пользоваться кодатой не очень удобно

Вот поэтому и использую ТС, а не просто джс. Пока получается

а в тс завезли проверку тотальности?

Ну, там вроде есть что-то типа элмовской проверки на варианты в свитч. Страдаю только от отсутствия полиморфизма функций (одноимённых) по типам - приходится использовать разные имена - и дата/кодата ссылка в этом чате просто всё разложила "по полочкам" в моей голове...

Пардон, а желание видеть эту книгу отрендеренной столь же неприлично, как желание ковырять Хаскель в IDE?

Навскидку - глазами виндузоида - чтобы с нею ознакомиться, надо ставить в виртуалку aж Coq
Или достаточно какой-то то гляделки tex?

навскидку Coq не требуется, только latexmk

думаю допишут - отрендерят

как вариант можно наверное каким нибудь онлайн сервисом воспользоваться

Советуют https://www.xm1math.net/texmaker/doc.html - оно читалка только по совместительству
Открываю book.tex, чтобы отрендерить предлагает выбор, выбираю Latex ругается на отсутствие лога
Как понять, какая там разновидность tex?

откройте ишью, думаю авторы лучше расскажут

Ога,
предлагают ставить полноценный latex c цыгвином
Притом не могут предложить чего-то конкретного, типа ставь что-то из трех дистров, первый из которых весит 250Мб

Попытался воззвать к голосу разума...
https://github.com/UniMath/SymmetryBook/issues/93

Вот, отрендерили и прислали. Действительно, обещают потом релизить, по мере готовности

Шо там?

Ну и впрямь бета-версия

Does that mean that a plane from the point of view of Euclidean geometry is not the same as a plane from the point of view of projective or affine geometry? Yes. These are of different types, because they have different notions of identification, and thus they have different properties.
Here we follow Quine’s dictum: No entity without identity! To know a type of objects is to know what it means to identify representatives of the type. The collection of self-identifications (self-transformations) of a given object form a group.
  ....
Groupoids vs groups. The type of all squares in a euclidean plane form a groupoid. It is connected, because between any two there exist identifications between them. But there is no canonical identification. When we say “the symmetry group of the square”, we can mean two things: 1) the symmetry group of a particular square; this is indeed a group, or 2) the connected groupoid of all squares; this is a “group up to conjugation”.
Vector spaces. Constructions and fields. Descartes and cartesian geometry.
  ....
All of mathematics is a tale, not about groups, but about ∞-groupoids. However, a lot of the action happens already with groups.

Да уж... Лучше энциклопедию юного математика почитать...

Ну, вторая глава - затравка о типах. И как-то это связано с остальным контентом

https://habr.com/ru/post/518206/

en src

https://writings.stephenwolfram.com/2020/04/finally-we-may-have-a-path-to-the-fundamental-theory-of-physics-and-its-beautiful/

Вольфрам или кто-нибудь умеет визуализировать теоркат? Хотя бы отчасти
Может, кто-то видел обучалки с визуализацией?
Ясно что денег на этом не заработаешь, только некоммерческое академическое..

Нет ничего лучше Милевского, но не хватает визуализации, и ему и студентам. Время утекает на мел и доску