nLab
product natural deduction - table

type theorycategory theory
syntaxsemantics
natural deductionuniversal construction
product typeproduct
type formationA:TypeB:TypeA×B:Type\frac{\vdash \;A \colon Type \;\;\;\;\; \vdash \;B \colon Type}{\vdash A \times B \colon Type}A,B𝒞A×B𝒞A,B \in \mathcal{C} \Rightarrow A \times B \in \mathcal{C}
term introductiona:Ab:B(a,b):A×B\frac{\vdash\; a \colon A\;\;\;\;\; \vdash\; b \colon B}{ \vdash \; (a,b) \colon A \times B} Q a (a,b) b A A×B B\array{ && Q\\ & {}^{\mathllap{a}}\swarrow &\downarrow_{\mathrlap{(a,b)}}& \searrow^{\mathrlap{b}}\\ A &&A \times B&& B }
term eliminationt:A×Bp 1(t):At:A×Bp 2(t):B\frac{\vdash\; t \colon A \times B}{\vdash\; p_1(t) \colon A} \;\;\;\;\;\frac{\vdash\; t \colon A \times B}{\vdash\; p_2(t) \colon B} Q t A p 1 A×B p 2 B\array{ && Q\\ &&\downarrow^{t} && \\ A &\stackrel{p_1}{\leftarrow}& A \times B &\stackrel{p_2}{\to}& B}
computation rulep 1(a,b)=ap 2(a,b)=bp_1(a,b) = a\;\;\; p_2(a,b) = b Q a (a,b) b A p 1 A×B p 2 B\array{ && Q \\ & {}^{\mathllap{a}}\swarrow &\downarrow_{(a,b)}& \searrow^{\mathrlap{b}} \\ A &\stackrel{p_1}{\leftarrow}& A \times B& \stackrel{p_2}{\to} & B}
Revised on September 29, 2012 02:40:58 by Mike Shulman (192.16.204.218)