From d5fbfe5f3a1a844b3205d2972d83d60cfe915c62 Mon Sep 17 00:00:00 2001
From: Hexirp <Hexirp@users.noreply.github.com>
Date: Sun, 2 May 2021 13:53:36 +0900
Subject: [PATCH] =?UTF-8?q?Add:=20=E9=80=B2=E3=82=81=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 type-theory/main.tex | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/type-theory/main.tex b/type-theory/main.tex
index 901a5f8..4e68ef1 100644
--- a/type-theory/main.tex
+++ b/type-theory/main.tex
@@ -1,6 +1,7 @@
 \documentclass[book]{jlreq}
 
 \usepackage{makeidx}
+\usepackage{bussproofs}
 \usepackage{color}
 \usepackage[colorlinks]{hyperref}
 
@@ -12,6 +13,9 @@
 \def\——{—\kern-.5\zw—\kern-.5\zw—}
 \newcommand{\bidash}{\——}
 \newcommand{\CIC}{\textsf{CIC}}
+\newcommand{\Type}{\mathrm{Type}}
+\newcommand{\Level}{\mathrm{Level}}
+\newcommand{\suc}{\mathrm{suc}}
 
 \begin{document}
 
@@ -42,7 +46,23 @@ \part{帰納的構造の計算}
 cardinals.''} \) と同じ無矛盾性を持つとか言われています。
 
 「帰納的構造の計算」は、 \index{Calculus of Inductive Constructions}``Calculus of Inductive Constructions'' を
-日本語に直訳した言葉です。これは \index{CIC@\CIC}\CIC とも略されます。
+日本語に直訳した言葉です。これは \index{CIC@\( \CIC \)}\( \CIC \) とも略されます。
+
+帰納的構造の計算には、\index{うちゅうかいそう@宇宙階層}宇宙階層が必要になります。これは、確か帰納型を含むことへの
+対価だったはずです。
+
+\index{Type@\( \Type \)}\( \Type \) は、一般的な型を表す記号です。 \index{Level@\( \Level \)}\( \Level \) は
+宇宙レベルの型を表す記号です。 \( i : \Level \) である時 \( \Type _ {i} \) と書き、これが一般的な形です。
+
+\begin{figure}[h]
+  \centering
+  \begin{prooftree}
+    \AxiomC{\( \)}
+    \UnaryInfC{\( i : \Level \vdash \Type _ {i} : \Type _ {\suc ( i )} \)}
+  \end{prooftree}
+  \caption{\( \Type _ {i} \) の型}
+  \label{cic-type-type}
+\end{figure}
 
 \backmatter