12,140
edits
Changes
MyWikiBiz, Author Your Legacy — Sunday November 02, 2025
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 04:06, 29 March 2009
, 04:06, 29 March 2009→Category 2: markup
===Category 2===
===Category 2===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
| E1. f 1_A = f,
<p>A ''category'' is a deductive system in which the following equations hold between proofs:</p>
|-
|
|
<p><math>\begin{array}{ll}
\text{E1.} & f 1_A = f, \qquad 1_B f = f, \qquad (hg)f = h(gf),
\\[8pt]
& \text{for all}~ f : A \to B, \quad g : B \to C, \quad h : C \to D.
\end{array}</math></p>
|-
|
|
<p>(Lambek & Scott, 52).
|
|}
===Cartesian Category===
===Cartesian Category===
