universe and observational equality

trees/def/def-004E.tree

@@ -0,0 +1,69 @@
+\title{Tarski Universe}
+\taxon{Definition}
+\import{macros}
+\p{
+    A \strong{universe} consists of a type #{\U} of which the elements are representations of types.
+    It is equipped with a type family #{\T} indexed by #{\U} called \strong{universal type family}.
+    The universe is closed under all the type constructors in the sense that it comes equipped with the following structure:
+    \ul{
+        \li{
+            #{\U} is closed under #{\Pi}, equipped with a function
+            ##{
+                \check{\Pi}:\Pi_{(X:\U)}(\T(X)\to\U)\to\U
+            }
+            for which the judgemental equality
+            ##{
+                \T(\check{\Pi}(X,P))\equiv\Pi_{(x:\T(X))}\T(P(x))
+            }
+            holds forall #{X:\U} and #{P:\T(X)\to\U}.
+        }
+        \li{
+            #{\U} is closed under #{\Sigma}, equipped with a function
+            ##{
+                \check{\Sigma}:\Pi_{(X:\U)}(\T(X)\to\U)\to\U
+            }
+            for which the judgemental equality
+            ##{
+                \T(\check{\Sigma}(X,P))\equiv\Sigma_{(x:\T(X))}\T(P(x))
+            }
+            holds forall #{X:\U} and #{P:\T(X)\to\U}.
+        }
+        \li{
+            #{\U} is closed under identity types, equipped with a function
+            ##{
+                \check{I}:\Pi_{(X:\U)}\T(X)\to\T(X)\to\U
+            }
+            for which the judgemental equality
+            ##{
+                \T(\check{I}(X,x,y))\equiv (x=y)
+            }
+            holds forall #{X:\U} and #{x,y:\T(X)}.
+        }
+        \li{
+            #{\U} is closed under coproducts, equipped with a function
+            ##{
+                \check{+}:\Pi_{(X:\U)}(\T(X)\to\U)\to\U
+            }
+            that satisfies the judgemental equality #{\T(X\check{+}P)\equiv\T(X)+\T(P)}
+        }
+        \li{
+            #{\U} contains elements #{\check{\unit}, \check{\void}, \check{\N} : \U} that satisfies the judgemental equality
+            ##{
+                \T(\check{\void})\equiv \void,
+                \\ \T(\check{\unit})\equiv \unit,
+                \\ \T(\check{\N})\equiv\N
+            }
+        }
+    }
+    Consider a universe #{\U} and a type #{A} in context #{\Gamma}.
+    We say that #{A} is a type in #{\U} or that #{\U} contains #{A},
+    if there is an element #{\check{A}:\U} such that #{\Gamma\vdash\T(\check{A})\equiv A\space\type} holds.
+}
+\subtree{
+    \title{Enough Universe}
+    \p{
+        Sometimes we may consider the universe #{\U} itself to be a type in some universes.
+        If we have only one #{\U}, the \strong{Russell Paradox} may arise.
+        Therefore we assume that there are \strong{enough universes}
+    }
+}

trees/def/def-004F.tree

@@ -0,0 +1,7 @@
+\title{Base Universe}
+\taxon{Definition}
+\import{macros}
+\p{
+    The \strong{base universee} #{\U_0} is defined using [universe postulate](thm-0013)
+    with empty context.
+}

trees/def/def-004G.tree

@@ -0,0 +1,19 @@
+\title{Successor Universe}
+\taxon{Definition}
+\import{macros}
+\p{
+    The \strong{successor universee} #{\U^+} of a universe #{\U} is defined using [universe postulate](thm-0013)
+    with the following contexts:
+    ##{
+        \vdash\U\space\type\quad X:\U\vdash\T(X)\space\type
+    }
+    It therefore contains the type #{\U} as well as type in #{\U}, in the following sense
+    ##{
+        \begin{align*}
+            &\vdash\check{\U}:\U^+\\ 
+            &\vdash\T^+(\check{\U})\equiv\U\type\\
+            &X:\U\vdash\check{\T}(X):\U^+\\ 
+            &X:\U\vdash\T^+(\check{\T}(X))\equiv\T(X)\type 
+        \end{align*}
+    }
+}

trees/def/def-004H.tree

@@ -0,0 +1,47 @@
+\import{macros}
+\title{Observational Equality of #{\N}}
+\taxon{Definition}
+\def\eqn{\text{Eq}}
+\p{
+    The observational equality of #{\N} is a binary relation #{\eqn_\N:\N\to(\N\to\U_0)} satisfies
+    ##{
+        \begin{align*}
+            \eqn_\N(0)(0) &\equiv \unit \\
+            \eqn_\N(0)(\succ(n)) &\equiv \void \\
+            \eqn_\N(\succ(m))(0) &\equiv \void \\
+            \eqn_\N(\succ(m))(\succ(n)) &\equiv \eqn_\N(m)(n)
+        \end{align*}
+    }
+    \proof{
+        We define #{\eqn} by double induction on #{\N}. By the first application of induction
+        it suffices to provide
+        ##{
+            \begin{align*}
+                &E_0:\N\to\U_0 \\ 
+                &E_S:\N\to((\N\to\U_0)\to(\N\to\U_0))
+            \end{align*}
+        }
+        we define #{E_0} by induction:
+        ##{
+            \begin{align*}
+                &E_0(0) \equiv\unit\\ 
+                &E_0(\succ(n)) \equiv\void
+            \end{align*}
+        }
+        and also define #{E_S} by induction:
+        ##{
+            \begin{align*}
+                &E_S(n,X,0)\equiv\void\\ 
+                &E_S(n,X,\succ(m))\equiv X(m)
+            \end{align*}
+        }
+        Therefore we have by the computation rule for the first induction that 
+        the following judgemental equality holds.
+        ##{
+            \begin{align*}
+                \eqn(0,m) &\equiv E_0(m) \\
+                \eqn(\succ(n),m) &\equiv E_S(n,\eqn(n),m)
+            \end{align*}
+        }
+    }
+}

trees/macros.tree

@@ -2,7 +2,7 @@
 \p{This file contains the basic macros used in the site.}
 \xmlns:html{http://www.w3.org/1999/xhtml}
 
-% Common utils
+% Layout utils
 \def\hr{\<html:hr>{}}
 \def\block[tit][body]{
     \subtree{
@@ -27,54 +27,60 @@
     }
   }
 }
+\def\proof[body]{
+ \scope{
+   \put\transclude/toc{false}
+   \subtree{
+     \taxon{proof}
+     \body
+   }
+ }
+}
+\def\graph[a]{
+    \tex{
+      \usepackage{tikz-cd}
+      \usepackage{amssymb}
+    }{
+        \a
+    }
+}
+\def\codeblock[lang][body]{
+  \pre{\<html:code>[class]{\lang}{\body}}
+}
 
-
-\def\sgn{\text{sgn}}
-\def\spn{\text{span}}
-\def\type{\space\text{type}}
+% Math fundamentals
 \def\N{\mathbb{N}}
 \def\Z{\mathbb{Z}}
 \def\Q{\mathbb{Q}}
 \def\R{\mathbb{R}}
 \def\C{\mathbb{C}}
 \def\F{\mathbb{F}}
+\def\U{\mathcal{U}}
+\def\T{\mathcal{T}}
+
+% Linear Algebra
+\def\sgn{\text{sgn}}
+\def\spn{\text{span}}
 \def\cl{\mathcal{L}}
 \def\set[a]{\{ \a \}}
-\def\succ{\text{succ}}
-\def\ind[a]{\text{ind}_\a}
-\def\indn{\text{ind}_\N}
-\def\indeq[a]{\text{ind-eq}_{\a}}
-\def\unit{\textbf{1}}
 \def\nulls{\text{null }}
 \def\range{\text{range }}
 \def\dom{\text{dom }}
 \def\cod{\text{cod }}
-\def\graph[a]{
-    \tex{
-      \usepackage{tikz-cd}
-      \usepackage{amssymb}
-    }{
-        \a
-    }
-}
-\def\proof[body]{
- \scope{
-   \put\transclude/toc{false}
-   \subtree{
-     \taxon{proof}
-     \body
-   }
- }
-}
-\def\refl{\text{refl}}
-\def\homset{\hom_\text{set}}
 \def\id{\text{id}}
-\def\pr[a]{\text{pr}_\a}
 \def\mat{\mathcal{M}}
+
+% Type Theory
+\def\type{\space\text{type}}
+\def\succ{\text{succ}}
+\def\refl{\text{refl}}
 \def\assoc{\text{assoc}}
-\def\codeblock[lang][body]{
-  \pre{\<html:code>[class]{\lang}{\body}}
-}
+\def\ind[a]{\text{ind}_\a}
+\def\indn{\text{ind}_\N}
+\def\indeq[a]{\text{ind-eq}_{\a}}
+\def\unit{\textbf{1}}
+\def\void{\textbf{0}}
+\def\pr[a]{\text{pr}_\a}
 
 % Lambda calculus
 \def\subt{\text{Sub}}
@@ -88,11 +94,10 @@
 \def\tob{\to_\beta}
 \def\tobm{\twoheadrightarrow_{\beta}}
 \def\etaeq{=_\eta}
+\def\norm[body]{\lVert\body\rVert}
 
 % category theory
 \def\obj{\text{Ob}}
 \def\mor{\text{Mor}}
 \def\cat{\mathbf{Cat}}
-
-% calculus
-\def\norm[body]{\lVert\body\rVert}
+\def\homset{\hom_\text{set}}

trees/thm/thm-0013.tree

@@ -0,0 +1,18 @@
+\title{Enough Universe}
+\taxon{Postulate}
+\import{macros}
+\p{
+    We assume that there're \strong{enough universe}, i.e.,
+    for every finite list of types in context 
+    ##{
+        \Gamma_1\vdash A_1\space\type,\cdots,\Gamma_n\vdash A_n\space\type
+    }
+    there is a universe #{\U} that contains each #{A_i} in the sense that #{\U} comes equipped with
+    ##{
+        \Gamma_i\vdash\check{A_i}:\U
+    }
+    for which the following judgement holds:
+    ##{
+        \Gamma_i \vdash\T(\check{A_i})\equiv A_i\space\type
+    }
+}

trees/tt/tt-0005.tree

@@ -1,6 +1,7 @@
 \title{Identity Types}
 \taxon{Type Theory}
 \date{2024-01-31}
+\import{macros}
 \p{
     This post discuss the identity types in type theory.
     Refer to [Introduction to Homotopy Type Theory](hott-2022).
@@ -52,3 +53,34 @@
     }
     \transclude{def-004D}
 }
+\subtree{
+    \title{Uniqueness of refl}
+    \p{
+        The identity type is an inductive family of types.
+        For instance, while the type #{a=x} indexed by #{x:A} is inductively generated by #{\refl_a},
+        the type #{a=a} is \strong{not}, because the endpoint of #{p:a=a} is not free. 
+        We want to show that #{p=\refl_a} for all #{p:a=a}. 
+    }
+    \p{
+        Nevertheless the identity type #{a=x} is generated by a single element #{\refl_a:a=a},
+        so it is natural to wonder in \em{what sense} the reflexivity identification is unique.
+        We prove that only one pair #{(a,\refl_a)} is unique in the type of all pairs:
+        ##{
+            (x,p):\Sigma_(x:A) a = x 
+        }
+        We restate this as a proposition: Consider an element #{a:A}. Then there is an identification
+        #{(a, \refl_a = y)} in the type #{\Sigma_(x:A) a = x} for any #{y:\Sigma_(x:A) a = x }
+    }
+    \proof{
+        By #{\Sigma} induction it suffices to show that there is an identification
+        ##{
+            (a, \refl_a) = (x, p)
+        }
+        forall #{x:A} and #{p:a=x}. Then perform the induction principle of identity types.
+        It suffices to show that
+        ##{
+            (a,\refl_a) = (a, \refl_a)
+        }
+        which can be obtained by reflexivity.
+    }
+}