Michael Shulman
product types in a 2-category

Unit type

Each sort has its own unit type, with the usual rules. For propositions, of course, the unit type is “true.”

1:nType(unit type)\frac{}{\vdash 1:n Type} (\text{unit type})

Strictly speaking, 11 should be decorated with an nn, but we generally omit that.

:1(unit term)\frac{}{\vdash \star:1} (\text{unit term})

x:1(x)(unit term is unique)\frac{}{x:1 \vdash (x\equiv \star)} (\text{unit term is unique})

Note that the presence of definitional equality makes the uniqueness easier to formulate. We also, of course, have to specify the arrows in the unit 1-type, which we do simply by saying that they form the unit 0-type.

(hom 1(,)1):Set(unit arrows)\frac{}{\vdash (hom_1(\star,\star) \equiv 1):Set} (\text{unit arrows})

Binary product types

Again, each sort has its own binary products.

ΓA:nTypeΓB:nTypeΓA×B:nType\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type} {\Gamma \vdash A\times B:n Type}

ΓA:nTypeΓB:nTypeΓx:AΓy:BΓx,y:A×B\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash x:A \qquad \Gamma \vdash y:B } {\Gamma \vdash \langle x,y\rangle:A\times B}

ΓA:nTypeΓB:nTypeΓz:A×BΓπ 1(z):A\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash z:A\times B } {\Gamma \vdash \pi_1(z):A}

ΓA:nTypeΓB:nTypeΓz:A×BΓπ 2(z):B\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash z:A\times B } {\Gamma \vdash \pi_2(z):B}

ΓA:nTypeΓB:nTypeΓx:AΓy:BΓ(π 1(x,y)x):A\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash x:A \qquad \Gamma \vdash y:B } {\Gamma \vdash (\pi_1(\langle x,y\rangle) \equiv x):A}

ΓA:nTypeΓB:nTypeΓx:AΓy:BΓ(π 2(x,y)y):B\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash x:A \qquad \Gamma \vdash y:B } {\Gamma \vdash (\pi_2(\langle x,y\rangle) \equiv y):B}

ΓA:nTypeΓB:nTypeΓz:A×BΓ(π 1(z),π 2(z)z):A×B\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type \qquad \Gamma \vdash z:A\times B } {\Gamma \vdash (\langle \pi_1(z),\pi_2(z)\rangle \equiv z):A\times B}

The above rules are all standard and apply the same at all levels. Of course, for propositions, ×\times is conjunction \wedge. However, for 1-types we also need to specify the arrows in a product, along with their composition and identities.

ΓA:CatΓB:CatΓ,x:A,x:A,y:B,y:B(hom A×B(x,y,x,y)hom A(x,x)×hom B(y,y)):Set\frac{\Gamma \vdash A:Cat \qquad \Gamma \vdash B:Cat} {\Gamma, x:A,x':A,y:B,y':B \vdash (hom_{A\times B}(\langle x,y\rangle, \langle x',y'\rangle) \equiv hom_A(x,x') \times hom_B(y,y')):Set}

ΓA:CatΓB:CatΓ,x:A,y:B(1 x,1 y1 x,y):hom A×B(x,y,x,y)\frac{\Gamma \vdash A:Cat \qquad \Gamma \vdash B:Cat} {\Gamma, x:A,y:B \vdash (\langle 1_x,1_y\rangle \equiv 1_{\langle x,y\rangle}):hom_{A\times B}(\langle x,y\rangle, \langle x,y\rangle)}

ΓA:CatΓB:CatΓ,x:A,x:A,x:A,f:hom A(x,x),f:hom A(x,x), y:B,y:B,y:B,g:hom B(y,y),g:hom B(y,y)(ff,gff,gf,g):hom A×B(x,y,x,y)\frac{\Gamma \vdash A:Cat \qquad \Gamma \vdash B:Cat} {\Gamma, \array{x:A,x':A,x'':A,f:hom_A(x,x'),f':hom_A(x',x''),\\ y:B,y':B,y'':B,g:hom_B(y,y'),g':hom_B(y',y'')} \vdash (\langle f'\circ f, g'\circ f\rangle \equiv \langle f',g'\rangle \circ \langle f,g\rangle):hom_{A\times B}(\langle x,y\rangle, \langle x'',y''\rangle)}
Created on March 10, 2010 20:09:37 by Mike Shulman (128.135.197.116)