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{}{⊢1:n\mathrm{Type}}(\text{unit type})$$\frac{}{\vdash 1:n Type} (\text{unit type})

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

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

$$\frac{}{x:1⊢(x\equiv \star )}(\text{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.

$$\frac{}{⊢({\mathrm{hom}}_1(\star ,\star )\equiv 1):\mathrm{Set}}(\text{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.

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

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢x:A\Gamma ⊢y:B}{\Gamma ⊢⟨x,y⟩:A\times 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}

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢z:A\times B}{\Gamma ⊢{\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_1(z):A}

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢z:A\times B}{\Gamma ⊢{\pi }_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}

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢x:A\Gamma ⊢y:B}{\Gamma ⊢({\pi }_1(⟨x,y⟩)\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_1(\langle x,y\rangle) \equiv x):A}

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢x:A\Gamma ⊢y:B}{\Gamma ⊢({\pi }_2(⟨x,y⟩)\equiv 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}

$$\frac{\Gamma ⊢A:n\mathrm{Type}\Gamma ⊢B:n\mathrm{Type}\Gamma ⊢z:A\times B}{\Gamma ⊢(⟨{\pi }_1(z),{\pi }_2(z)⟩\equiv z):A\times 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 ⊢A:\mathrm{Cat}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,x:A,x\prime :A,y:B,y\prime :B⊢({\mathrm{hom}}_{A\times B}(⟨x,y⟩,⟨x\prime ,y\prime ⟩)\equiv {\mathrm{hom}}_A(x,x\prime )\times {\mathrm{hom}}_B(y,y\prime )):\mathrm{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}

$$\frac{\Gamma ⊢A:\mathrm{Cat}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,x:A,y:B⊢(⟨1_x,1_y⟩\equiv 1_{⟨x,y⟩}):{\mathrm{hom}}_{A\times 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)}

$$\frac{\Gamma ⊢A:\mathrm{Cat}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,\begin{array}{c}x:A,x\prime :A,x″:A,f:{\mathrm{hom}}_A(x,x\prime ),f\prime :{\mathrm{hom}}_A(x\prime ,x″),\\ y:B,y\prime :B,y″:B,g:{\mathrm{hom}}_B(y,y\prime ),g\prime :{\mathrm{hom}}_B(y\prime ,y″)\end{array}⊢(⟨f\prime \circ f,g\prime \circ f⟩\equiv ⟨f\prime ,g\prime ⟩\circ ⟨f,g⟩):{\mathrm{hom}}_{A\times 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)}