Leanの論理再考 3

Lean 論理

\require{color}% \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1]{ \langle\![{#1}]\!\rangle }% \newcommand{\As}{\;::\;}% \newcommand{\HR}[1]{ \rule[0.5ex]{#1}{0.5pt} }% %\newcommand{\HR}[1]{\Rule{#1}{0.6ex}{-0.5ex} }% \newcommand{\cat}[1]{\mathcal{#1}}% \newcommand{\IN}{\mbox{ in }}%

なんかのバグで水平線が表示されたり、されなかったり。ドットが水平線の場所。ブラウザにも依存するようだ。なんだよコレ

型構成＝対象構成

依存型理論：
x:X \vdash F(x):Type \\ .\HR{10em}\;[\Pi] \\ \Pi x:X. F(x) : Type

対応する圏論：
F:\llcorner X\lrcorner \to \cat{C} \IN {\bf CAT} \\ .\HR{10em}\;[Lim] \\ Lim_{\llcorner X\lrcorner}(F) \in |\cat{C}|

関数データ構成＝ポイント射構成

依存型理論：
x:X \vdash \psi_x:F(x) \\ .\HR{15em}\;[\lambda ] \\ \lambda\, x:X. \psi_x : \Pi x:X.F(x)

対応する圏論：
\psi:: K_{\bf 1} \Rightarrow F: \llcorner X\lrcorner \to \cat{C} \IN {\bf CAT} \\ .\HR{15em}\;[\Lambda ] \\ \Lambda(\psi):{\bf 1} \to Lim_{\llcorner X\lrcorner}(F) \in |\cat{C}|