glue

groupoid · Oct 30, 2023 · 7e60549 · 7e60549
1 parent 3d644e0
commit 7e60549
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/intro/index.html b/intro/index.html
@@ -10,8 +10,10 @@
 <a href='#'>INTRO</a></nav><article class="main"><div class="exe"><section><h1>Теорія типів</h1><span></span></section></div><aside><time>Код курсу: КМ-111-10<br>Кількість кредитів: 12</time></aside><div class="exe"><section><h2>Вступ в предмет</h2><p>Теорія типів — це універсальна мова програмування чистої
 математики (для доведення теорем),
 яка може містити довільну кількість консистентних аксіом,
-впорядкованих у вигляді ізоморфізмів: функцій encode і decode та
-їх рівнянь — бета і ета правил обчислювальності та унікальності (секції та ретракту).
+впорядкованих у вигляді псевдо-ізоморфізмів:
+функцій encode (способи конструювання елементів типу)
+і decode (залежні елімінатори універсального принципу індукції типу) та
+їх рівнянь — бета і ета правил обчислювальності та унікальності.
 Зазвичай теорія типів вже постачається з наступними типами (примітивами-аксіомами)
 та коментарями у вигляді окремих лекцій (конспекти):</p><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0.124ex;" xmlns="http://www.w3.org/2000/svg" width="1.131ex" height="0.88ex" role="img" focusable="false" viewBox="0 -444 500 389" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1419-TEX-N-2219" d="M55 251Q55 328 112 386T249 444T386 388T444 249Q444 171 388 113T250 55Q170 55 113 112T55 251Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo"><use data-c="2219" xlink:href="#MJX-1419-TEX-N-2219"></use></g></g></g></svg></mjx-container> <a href="../foundations/mltt/pi/index.html">Простори функцій</a> (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="2.036ex" height="1.538ex" role="img" focusable="false" viewBox="0 -680 900 680" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1420-TEX-B-1D6B7" d="M400 0Q376 3 226 3Q75 3 51 0H39V62H147V618H39V680H860V618H752V62H860V0H848Q824 3 674 3Q523 3 499 0H487V62H595V618H304V62H412V0H400Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D6B7" xlink:href="#MJX-1420-TEX-B-1D6B7"></use></g></g></g></g></svg></mjx-container>)<br>
 <mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0.124ex;" xmlns="http://www.w3.org/2000/svg" width="1.131ex" height="0.88ex" role="img" focusable="false" viewBox="0 -444 500 389" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1421-TEX-N-2219" d="M55 251Q55 328 112 386T249 444T386 388T444 249Q444 171 388 113T250 55Q170 55 113 112T55 251Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="mo"><use data-c="2219" xlink:href="#MJX-1421-TEX-N-2219"></use></g></g></g></svg></mjx-container> <a href="../foundations/mltt/sigma/index.html">Простори пар</a> (<mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: 0;" xmlns="http://www.w3.org/2000/svg" width="1.88ex" height="1.552ex" role="img" focusable="false" viewBox="0 -686 831 686" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1422-TEX-B-1D6BA" d="M766 271Q764 266 750 137T735 4V0H407Q74 0 71 4L70 5Q64 9 64 18Q64 24 82 41T213 158L359 288Q360 288 320 336T214 460Q67 633 66 635Q64 638 64 655Q64 679 75 684Q78 686 407 686H735V682Q738 676 751 558T766 434V430H735Q704 430 704 431Q704 434 703 444T696 477T681 520T654 563T613 598Q578 615 527 619T371 624H281L396 489Q506 358 513 351Q517 342 512 334Q503 325 371 208Q338 179 303 147T249 99L231 83L243 81Q258 81 364 81Q382 81 418 81T470 82T513 83T554 88T587 96T619 109T645 129Q689 173 702 260L704 274Q704 275 735 275H766V271Z"></path></defs><g stroke="currentColor" fill="currentColor" stroke-width="0" transform="scale(1,-1)"><g data-mml-node="math"><g data-mml-node="TeXAtom" data-mjx-texclass="ORD"><g data-mml-node="mi"><use data-c="1D6BA" xlink:href="#MJX-1422-TEX-B-1D6BA"></use></g></g></g></g></svg></mjx-container>)<br>

diff --git a/intro/index.pug b/intro/index.pug
@@ -28,8 +28,10 @@ block content
                     Теорія типів — це універсальна мова програмування чистої
                     математики (для доведення теорем),
                     яка може містити довільну кількість консистентних аксіом,
-                    впорядкованих у вигляді ізоморфізмів: функцій encode і decode та
-                    їх рівнянь — бета і ета правил обчислювальності та унікальності (секції та ретракту).
+                    впорядкованих у вигляді псевдо-ізоморфізмів:
+                    функцій encode (способи конструювання елементів типу)
+                    і decode (залежні елімінатори універсального принципу індукції типу) та
+                    їх рівнянь — бета і ета правил обчислювальності та унікальності.
                     Зазвичай теорія типів вже постачається з наступними типами (примітивами-аксіомами)
                     та коментарями у вигляді окремих лекцій (конспекти):
                 +tex.

diff --git a/lib/foundations/univalent/equiv.anders b/lib/foundations/univalent/equiv.anders
@@ -17,7 +17,6 @@
 
 module equiv where
 import lib/foundations/univalent/path
-option girard true
 
 --- [Pelayo, Warren] 2012
 
@@ -51,6 +50,8 @@ def univ-computation (A B : U) (p : PathP (<_> U) A B)
 
 --- Equiv as [Right] Identity System [Escardó] 2014
 
+option girard true
+
 def single (B : U) : U := Σ (A: U), equiv A B
 def idEquiv≡ (A : U) (y : single A) : Path (single A) (A, idEquiv A) y := ?
 def unglueEquiv (A : U) (φ : I) (f : Partial (single A) φ) : equiv (Glue A φ f) A := ?