XyJaxを使った例
$`\xymatrix@R-1.8pc@C-2pc{
{}
&*{A:Type}
&
&*{a:A \vdash F(a):Type}
&
\\
{}\ar@{-}[rrrr]
&
&
&
&
\\
{}
&
&* {\prod_{a:A}F(a) : Type}
&
}`$
\xymatrix@R-1.8pc@C-2pc{ {} &*{A:Type} & &*{a:A \vdash F(a):Type} & \\ {}\ar@{-}[rrrr] & & & & \\ {} & &* {\prod_{a:A}F(a) : Type} & }
色付きテキスト方式
マクロ：$`\require{color}%
\newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }%
\newcommand{\When}{\Keyword{when\:\:} }%
\newcommand{\And}{ \Keyword{\:\: and \:\:} }%
\newcommand{\Then}{ \Keyword{then\: } }%
\newcommand{\Holds}{ \Keyword{holds\:\:} }%
\newcommand{cat}[1]{ \mathcal{#1} }%
`$
\require{color}% \newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }% \newcommand{\When}{\Keyword{when\:\:} }% \newcommand{\And}{ \Keyword{\:\: and \:\:} }% \newcommand{\Then}{ \Keyword{then\: } }% \newcommand{\Holds}{ \Keyword{holds\:\:} }% \newcommand{cat}[1]{ \mathcal{#1} }%
$`\When A:Type \And a: A \vdash F(a):Type \\
\Then \\
\Holds \prod_{a:A}F(a) : Type
`$
\When A:Type \And a: A \vdash F(a):Type \\ \Then \\ \Holds \prod_{a:A}F(a) : Type
