デカルト閉・型システム

$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{-}}
\newcommand{\u}[1]{\overline{#1} }
\newcommand{\Ev}{\triangleleft}
\newcommand{\In}{\text{ in } }
`$

$`/\cat{C}/ = (|\cat{C}|, \times, \to, \u{(\hyp)}, \Ev)`$

  1. $`(\times) : |\cat{C}|\times |\cat{C}| \to |\cat{C}| \In {\bf SET}`$
  2. $`(\to) : |\cat{C}|\times |\cat{C}| \to |\cat{C}| \In {\bf SET}`$
  3. $`\u{(\hyp)} : |\cat{C}| \to |{\bf Set}| \In {\bf SET}`$
  4. $`(\Ev) \in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\u{A \to B} \times \u{A}, \u{B})`$

$`(\hyp)_{A, B}^\wedge : \cat{C}(A, B) \to \u{A \to B} \In {\bf Set}\\
(\hyp)^{A,B}_\vee : \u{A \to B} \to \cat{C}(A, B) \In {\bf Set}
`$

$`(\hyp)^\wedge \in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\cat{C}(A, B), \u{A \to B})\\
(\hyp)_\vee\in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\u{A \to B}, \cat{C}(A, B))
`$

$`a : A \In /\cat{C}/ \iff a \in \u{A} \In {\bf Set}\\
f : A \to B \In /\cat{C}/ \iff f \in \u{A\to B} \In {\bf Set}
`$