帰納的にデータ型を定義するとき：$`\require{color} % Using
\newcommand{\NN}[1]{ \textcolor{orange}{\text{#1}} } % New Name
\newcommand{\NX}[1]{ \textcolor{orange}{#1} } % New EXpression
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\B}[1]{ \mathbf{#1} }
\newcommand{\N}[1]{ \textcolor{blue}{\text{#1}} } % Name
\newcommand{\dto}{ \mathrel{!\!\!\to}}
\newcommand{\dtimes}{ \mathop{!\!\times} }
`$
$`\T{volatile namespace}\\
\T{we define type }\NN{Nat}\\
\T{applying inductive}\\
\quad \NN{0} : \T{Nat}\\
\quad \NN{s} : \T{Nat} \to \T{Nat}\\
\T{end definition}\\
\T{end namespace}
`$
https://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf から、コンテキストとタイプの相互再帰的な定義：
$`
\T{data } \NN{Con} : \T{Set}\\
\T{data } \NN{Ty} : \T{Con} \to \T{Set}\\
\T{data } \N{Con} \T{ where}\\
\quad \NX{\bullet} : \T{Con}\\
\quad \NX{(\_ ,\_) } : (\Gamma : \T{Con}) → \T{Ty}\, \Gamma \to \T{Con}\\
\T{data } \N{Ty} \T{ where}\\
\quad \NN{ U } : \forall \{\Gamma\} \to \T{Ty}\, \Gamma\\
\quad \NX{\Pi} : \forall\{\Gamma\} (A : \T{Ty}\, \Gamma)\, (B : \T{Ty}\, (\Gamma , A)) \to \T{Ty} \,\Gamma
`$
これをより分かりやすく書く。
$`
\T{we declare type } \NN{Con} \T{ in the universe } |\B{Set}|\\
\T{we declare type-family } \NN{Ty} \\
\quad \T{for } \Gamma : \T{Con} \\
\quad \T{returns a type in the universe } |\B{Set}|\\
\T{end}\\
\:\\
\T{we define type } \N{Con} \T{ together with } \N{Ty}\\
\T{applying inductive}\\
\quad \NX{\diamond} : \T{Con}\\
\quad \NX{(\_ \cdot\_) } : (\Gamma : \T{Con}) \dto (\T{Ty}(\Gamma) \to \T{Con})\\
\T{end}\\
\T{we define type-family } \N{Ty} \T{ together with }\N{Con}\\
\T{applying inductive}\\
\quad \NN{ U } : \{\Gamma : \T{Con}\} \dto \T{Ty}(\Gamma) \T{ // unit type}\\
\T{/* pi type */}\\
\quad \NX{\Pi} : \{\Gamma:\T{Con}\} \dto \left( (A : \T{Ty}(\Gamma) ) \dtimes (B : \T{Ty}(\Gamma \cdot A)) \dto \T{Ty}(\Gamma) \right)\\
\T{end}
`$
要点は：
- 誤解を招かないキーワードを使う。
- 型と型ファミリーを区別する。
- 演算子記号や関係記号の優先順位に頼らない。
- カンマや空白を演算子記号として使わない。
- 総じて、無闇と省略はしない。
