$`\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\…

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@{-}[rrr…