具体的にどのように実現してるかは後で書きます
$$ \gdef\U{\mathcal{U}} \gdef\isProp{\mathrm{isProp}} \gdef\rec{\mathrm{rec}} $$おいっす
こういうのを書くと、
1```math
2\begin{tikzcd}
3 {F^{n+2}0} && {F^{n+1}0} && {F^n0} \\ \\
4 {F^2A} && FA && A
5 \arrow["{F^2f_n}", from=1-1, to=3-1]
6 \arrow["{Ff_{n+1}}", from=1-1, to=3-3]
7 \arrow["{F^{n+1}!}"', from=1-3, to=1-1]
8 \arrow["{Ff_n}", from=1-3, to=3-3]
9 \arrow["{f_{n+1}}", from=1-3, to=3-5]
10 \arrow["{F^n!}"', from=1-5, to=1-3]
11 \arrow["{f_n}", from=1-5, to=3-5]
12 \arrow["{F\alpha}"', from=3-1, to=3-3]
13 \arrow["\alpha"', from=3-3, to=3-5]
14\end{tikzcd}
15```
↓ こういうSVGになります
プリアンブルもあるよ〜
1\newcommand{\U}{\mathcal{U}}
2\newcommand{\isProp}{\mathrm{isProp}}
3\newcommand{\rec}{\mathrm{rec}}
1```math
2$\displaystyle \rec_{\|A\|} : \prod_{X : \U} \isProp(X) \to (A \to X) \to \|A\| \to X$
3```
でもこういう普通の数式を使いたいときには色々不便なので普通にKaTeXを使った方がよいですね サイズもデカすぎるし
$$ \rec_{\|A\|} : \prod_{X : \U} \isProp(X) \to (A \to X) \to \|A\| \to X $$1```math
2\begin{tikzcd}
3 \|A\| & |[font=\footnotesize]| (\text{when } h : \isProp(X)) \\
4 A & X
5 \arrow["|-|", from=2-1, to=1-1]
6 \arrow["f", from=2-1, to=2-2]
7 \arrow["{\rec_{\|A\|}(h, f)}" near end, from=1-1, to=2-2, dashed]
8\end{tikzcd}
9```