інтро

groupoid · Oct 20, 2023 · 625b398 · 625b398
1 parent 2e3533c
commit 625b398
Show file tree

Hide file tree

Showing 36 changed files with 907 additions and 905 deletions.
diff --git a/foundations/mltt/either/index.html b/foundations/mltt/either/index.html
@@ -7,5 +7,5 @@
 use[data-c]{stroke-width:3px}
 </style></head><body class="content"></body></html><html><head><meta property="og:title" content="EITHER"><meta property="og:description" content="Either type (disjunction)"><meta property="og:url" content="https://anders.groupoid.space/foundations/mltt/either/"></head></html><title>EITHER</title><nav><a href='https://anders.groupoid.space/'>ANDERS</a>
 <a href='https://anders.groupoid.space/lib/'>LIB</a>
-<a href='#'>EITHER</a></nav><article class="main list"><section><h1>EITHER</h1><aside><time>Published: 16 OCT 2017</time></aside><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.186ex;" xmlns="http://www.w3.org/2000/svg" width="1.76ex" height="1.505ex" role="img" focusable="false" viewBox="0 -583 778 665" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1490-TEX-N-2B" d="M56 237T56 250T70 270H369V420L370 570Q380 583 389 583Q402 583 409 568V270H707Q722 262 722 250T707 230H409V-68Q401 -82 391 -82H389H387Q375 -82 369 -68V230H70Q56 237 56 250Z"></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="2B" xlink:href="#MJX-1490-TEX-N-2B"></use></g></g></g></svg></mjx-container>-type is a representation disjunction.
+<a href='#'>EITHER</a></nav><article class="main list"><section><h1>EITHER</h1><aside><time>Published: 16 OCT 2017</time></aside><p><mjx-container class="MathJax" jax="SVG"><svg style="vertical-align: -0.186ex;" xmlns="http://www.w3.org/2000/svg" width="1.76ex" height="1.505ex" role="img" focusable="false" viewBox="0 -583 778 665" xmlns:xlink="http://www.w3.org/1999/xlink"><defs><path id="MJX-1-TEX-N-2B" d="M56 237T56 250T70 270H369V420L370 570Q380 583 389 583Q402 583 409 568V270H707Q722 262 722 250T707 230H409V-68Q401 -82 391 -82H389H387Q375 -82 369 -68V230H70Q56 237 56 250Z"></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="2B" xlink:href="#MJX-1-TEX-N-2B"></use></g></g></g></svg></mjx-container>-type is a representation disjunction.
 </p><h2>Constructors</h2><h2>Eliminators</h2><h2>Induction Principle</h2></section></article><footer class="footer"><a href="https://5ht.co/license/"><img class="footer__logo" src="https://longchenpa.guru/seal.png" width="50"></a><span class="footer__copy">2021&mdash;2023 &copy; <a href="//groupoid.space/" style="color:Lavender;">Groupoïd Infinity</a></span></footer>
diff --git a/foundations/mltt/id/index.html b/foundations/mltt/id/index.html
diff --git a/foundations/mltt/id/index.pug b/foundations/mltt/id/index.pug
@@ -97,8 +97,9 @@ block content
                 def UIP (A : V) (a b : A) (p q : Id A a b)
                   : Id (Id A a b) p q
                  := ref p
+            br.
 
-            h2 THEOREMS
+            h1 THEOREMS
 
             +tex.
                 $\mathbf{Definition}$ (Identity System). An identity system

diff --git a/foundations/mltt/inductive/index.html b/foundations/mltt/inductive/index.html
diff --git a/foundations/mltt/inductive/index.pug b/foundations/mltt/inductive/index.pug
@@ -35,9 +35,7 @@ block content
                 def F:            ℕ → U := ℕ-iter U 𝟎 (+ 𝟏)
             br.
             +tex.
-                Library includes definitions for other
-                disjunction ranks $𝟑,$ $𝟒,$ $𝟓,$ $𝟔,$ $𝟕$ with
-                ballanced packing, like $𝟕=𝟑+𝟒$, $𝟓=𝟐+𝟑$, $𝟔=𝟑+𝟑$. For multiple
+                For multiple
                 occurance of fixpoint variable in W-fiber encoded
                 argument use $×$ cartesian product, like for binary trees 𝟏 × 𝟏.
                 Here is example for List MLTT encoding:
@@ -58,15 +56,15 @@ block content
 
             h2 Formation
             +tex.
-                $\mathbf{Definition}$ (Empty). Empty-type is defined as built-in 𝟎-type:
+                $\mathbf{Definition\ 4.1}$ (Empty). Empty-type is defined as built-in 𝟎-type:
             +tex(true).
                 $$
                     𝟎 : \mathcal{U}.
                 $$
 
             h2 Elimination
             +tex.
-                $\mathbf{Definition}$ (Induction Principle $\mathrm{ind_0}$). 𝟎-type is satisfying the
+                $\mathbf{Definition\ 4.2}$ (Induction Principle $\mathrm{ind_0}$). 𝟎-type is satisfying the
                 induction principle:
 
             +code.
@@ -77,7 +75,7 @@ block content
                 $$
 
             +tex.
-                $\mathbf{Definition}$ (Negation or isEmpty). For any type A negation of A is defined as arrow from A to 𝟎:
+                $\mathbf{Definition\ 4.2.1}$ (Negation or isEmpty). For any type A negation of A is defined as arrow from A to 𝟎:
             +tex(true).
                 $$
                     \neg A := A \rightarrow 𝟎.
@@ -102,7 +100,7 @@ block content
             h2 Formation
 
             +tex.
-                $\mathbf{Definition}$ (Unit). Unit-type is defined as built-in 𝟏-type:
+                $\mathbf{Definition\ 4.3}$ (Unit). Unit-type is defined as built-in 𝟏-type:
             +tex(true).
                 $$
                     𝟏 : \mathcal{U}.
@@ -111,7 +109,7 @@ block content
             h2 Introduction
 
             +tex.
-                $\mathbf{Definition}$ (Star). 𝟏-type containts single inhabitant ★:
+                $\mathbf{Definition\ 4.4}$ (Star). 𝟏-type containts single inhabitant ★:
             +tex(true).
                 $$
                     ★ : 𝟏.
@@ -120,7 +118,7 @@ block content
             h2 Elimination
 
             +tex.
-                $\mathbf{Definition}$. (Induction Principle $\mathrm{ind_1}$). 𝟏-type satisfies
+                $\mathbf{Definition\ 4.5}$. (Induction Principle $\mathrm{ind_1}$). 𝟏-type satisfies
                 induction principle that for any family $C$ indexed by $x : 1$ there is a function
             +code.
                 def 1-ind (C: 𝟏 → U) (x: C ★) (z: 𝟏) : C z := ind₁ C x z
@@ -130,13 +128,15 @@ block content
                 $$
 
             h2 Computation
-
             +tex.
-                $\mathbf{Theorem}$ (Unit Computes). The following equation holds:
+                $\mathbf{Theorem\ 4.6}$ (Unit Computes). The following equation holds:
             +tex(true).
                 $$
                    \mathrm{ind_1}(x,★) = x.
                 $$
+            h2 Uniqueness
+            +tex.
+                $\mathbf{Theorem\ 4.7}$ (Unit Unique).
 
             h1 BOOL
 
@@ -147,7 +147,7 @@ block content
             h2 Formation
 
             +tex.
-                $\mathbf{Definition}$ (Bool). Boolean-type or 0-sphere is defined as built-in 𝟐-type:
+                $\mathbf{Definition\ 4.8}$ (Bool). Boolean-type or 0-sphere is defined as built-in 𝟐-type:
             +tex(true).
                 $$
                     𝟐 : \mathcal{U}.
@@ -156,14 +156,14 @@ block content
             h2 Introduction
 
             +tex.
-                $\mathbf{Definition}$ ($0_2$). false or $0_2$.
+                $\mathbf{Definition\ 4.9}$ ($0_2$). false or $0_2$.
             +tex(true).
                 $$
                     0_2 : 𝟐.
                 $$
 
             +tex.
-                $\mathbf{Definition}$ ($1_2$). true or $1_2$.
+                $\mathbf{Definition\ 4.10}$ ($1_2$). true or $1_2$.
             +tex(true).
                 $$
                     1_2 : 𝟐.
@@ -172,7 +172,7 @@ block content
             h2 Elimination
 
             +tex.
-                $\mathbf{Definition}$ (Induction Principle $\mathrm{ind_2}$).
+                $\mathbf{Definition\ 4.11}$ (Induction Principle $\mathrm{ind_2}$).
             +code.
                 def 2-ind (C: 𝟐 → U) (x: C 0₂) (y: C 1₂) (z: 𝟐) : C z := ind₂ C x y z
             +tex(true).
@@ -188,7 +188,7 @@ block content
             h2 Formation
 
             +tex.
-                $\mathbf{Definition}$ ($\mathrm{W}$-Formation). For $A : \mathcal{U}$ and $B : A \rightarrow \mathcal{U}$, type $\mathrm{W}$
+                $\mathbf{Definition\ 4.12}$ ($\mathrm{W}$-Formation). For $A : \mathcal{U}$ and $B : A \rightarrow \mathcal{U}$, type $\mathrm{W}$
                 is defined as $\mathrm{W}(A,B) : \mathcal{U}$ or
             code.
                 def W' (A : U) (B : A → U) : U := W (x : A), B x
@@ -200,7 +200,7 @@ block content
             h2 Introduction
 
             +tex.
-                $\mathbf{Definition}$ ($\mathrm{W}$-Introduction). Elements of $\mathrm{W}_{(x : A)} B(x)$ are called
+                $\mathbf{Definition\ 4.13}$ ($\mathrm{W}$-Introduction). Elements of $\mathrm{W}_{(x : A)} B(x)$ are called
                 well-founded trees and created with single $\mathrm{sup}$ constructor:
 
             code.
@@ -216,7 +216,7 @@ block content
             h2 Elimination
 
             +tex.
-                $\mathbf{Definition}$ (Induction Principle $\mathrm{ind^W}$). The induction principle states that
+                $\mathbf{Definition\ 4.14}$ (Induction Principle $\mathrm{ind^W}$). The induction principle states that
                 for any types $A: \mathcal{U}$ and $B: A \rightarrow \mathcal{U}$ and type family $C$ over $\mathrm{W}(A,B)$
                 and the function $g : G$, where
 
@@ -242,7 +242,7 @@ block content
             h2 Computation
 
             +tex.
-                $\mathbf{Theorem}$ ($\mathrm{ind^W}$ computes). The induction principle $\mathrm{ind^W}$ satisfies
+                $\mathbf{Theorem\ 4.15}$ ($\mathrm{ind^W}$ computes). The induction principle $\mathrm{ind^W}$ satisfies
                 the equation:
             +code.
                 def indᵂ-β (A : U) (B : A → U)
@@ -253,10 +253,14 @@ block content
                           (indᵂ A B C g (sup A B a f))
                           (g a f (λ (b : B a), indᵂ A B C g (f b)))
                  := <_> g a f (λ (b : B a), indᵂ A B C g (f b))
+            br.
             +tex(true).
                 $$
                     \mathrm{ind^W_\beta} : g(a,f,λb.\mathrm{ind^W}(g,f(b))) = \mathrm{ind^W}(g,\mathrm{sup}(a,f)).
                 $$
+            h2 Uniqueness
 
+            +tex.
+                $\mathbf{Theorem\ 4.16}$ ($W$-Uniqueness).
 
 include ../../../footer