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.”

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

Strictly speaking, $1$ should be decorated with an $n$, but we generally omit that.

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

$$\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.

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

Binary product types

Again, each sort has its own binary products.

$$\frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type} {\Gamma \vdash A\times B:n Type}$$

$$\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}$$

$$\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}$$

$$\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}$$

$$\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}$$

$$\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}$$

$$\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.

$$\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}$$

$$\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)}$$

$$\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)}$$