Merge branch 'main' of github.com:groupoid/anders

Author: 5HT

intro/CANONICITY.md

@@ -4,12 +4,12 @@ Canonicity
 # Prolog
 
 Я називаю це трьома станами в'язкості (синтаксичне, пропозиційне і гомотопічне) мислення,
-які існують у чотирьох глибинах (категорії, йоги гротендіка, когомології, супергеометрія).
-
-Спочатку зі стану MLTT де мислення залізобетонне (тому що обмежене) і в мандалі ви відчуваєте фібраційне дихання ви занурюєтеся в ідентифікаційні простори, а потім згодом відзнаходите числення у самих ідентифікаціях розуміючи шо мислення існує з дірками, які не обчислюються.
+які існують у чотирьох глибинах (категорії, йоги Гротендіка, когомології, супергеометрія).
 
+Спочатку зі стану MLTT де мислення залізобетонне (тому що обмежене) і в мандалі ви відчуваєте
+фібраційне дихання ви занурюєтеся в ідентифікаційні простори, а потім згодом відзнаходите
+числення у самих ідентифікаціях розуміючи шо мислення існує з дірками, які не обчислюються.
 Де закони нормалізації ускладнюють візерунки так швидко і так складно, що психіка наче тоне у болоті гомотопічної в'язкості.
-
 Останній спосіб мислення ілімінує повністю всі гомотопічні рівності в цій системі бескінечних всесвітів двох типів.
 
 Загалом наше мислення може робити помилки тільки таких типів:
@@ -282,5 +282,5 @@ path-dependent constructions is entirely unworkable. Instead, it means that:
   of `ℕ` that avoid the pitfalls of higher inductive types while still
   respecting constructive and homotopical principles.
 
-* Direct inductive definition of `ℕ`: One way to preserve canonicity is to define
+* Direct inductive definition of `ℕ`: One way to preserve canonicity is to define by general induction or built-in.