12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Wednesday May 01, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 04:40, 29 March 2009
, 04:40, 29 March 2009→Cartesian Category: markup
===Cartesian Category===
===Cartesian Category===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| E2. f = O_A, for all f : A -> T.
<p>A ''cartesian category'' is both a category and a conjunction calculus satisfying the additional equations:</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{E2.} & f = \bigcirc_A, \quad \text{for all}~ f : A \to \operatorname{T};
\\[8pt]
\text{E3a.} & \pi^{}_{A,B} \langle f, g \rangle = f,
\\[8pt]
\text{E3b.} & \pi^\prime_{A,B} \langle f, g \rangle = g,
\\[8pt]
\text{E3c.} & \langle \pi^{}_{A,B} h, \pi^\prime_{A,B} h \rangle = h,
\\[8pt]
& \text{for all}~ f : C \to A, \quad g : C \to B, \quad h : C \to A \land B.
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 52).</p>
|}
|
===Cartesian Closed Category===
===Cartesian Closed Category===
