12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 05:34, 29 March 2009
, 05:34, 29 March 2009→Cartesian Closed Category: markup
===Cartesian Closed Category===
===Cartesian Closed Category===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>A ''cartesian closed category'' is a cartesian category <math>\mathcal{A}</math> with additional structure <math>\text{R4}\!</math> satisfying the additional equations:</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{E4a.} & \varepsilon^{}_{A,B} \langle h^* \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle = h,
\\[8pt]
\text{E4b.} & (\varepsilon^{}_{A,B} \langle k \pi^{}_{C,B}, \pi^\prime_{C,B} \rangle)^* = k,
\\[8pt]
& \text{for all}~ h : C \land B \to A \quad \text{and} \quad k : C \to (A \Leftarrow B).
\end{array}</math></p>
|-
|
|
<p>Thus, a cartesian closed category is a positive intuitionistic propositional calculus satisfying the equations <math>\text{E1}\!</math> to <math>\text{E4}.\!</math> This illustrates the general principle that one may obtain interesting categories from deductive systems by imposing an appropriate equivalence relation on proofs.</p>
<p>(Lambek & Scott, 53).</p>
|}
</pre>
==Document History==
==Document History==