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}}\left(\text{unit type}\right)$\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}\left(\text{unit term}\right)$\frac{}{\vdash \star:1} (\text{unit term})

$\frac{}{x:1⊢\left(x\equiv \star \right)}\left(\text{unit term is unique}\right)$\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{}{⊢\left({\mathrm{hom}}_{1}\left(\star ,\star \right)\equiv 1\right):\mathrm{Set}}\left(\text{unit arrows}\right)$\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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}}{\Gamma ⊢A×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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢x:A\phantom{\rule{2em}{0ex}}\Gamma ⊢y:B}{\Gamma ⊢⟨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}

$\frac{\Gamma ⊢A:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢z:A×B}{\Gamma ⊢{\pi }_{1}\left(z\right):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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢z:A×B}{\Gamma ⊢{\pi }_{2}\left(z\right):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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢x:A\phantom{\rule{2em}{0ex}}\Gamma ⊢y:B}{\Gamma ⊢\left({\pi }_{1}\left(⟨x,y⟩\right)\equiv x\right):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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢x:A\phantom{\rule{2em}{0ex}}\Gamma ⊢y:B}{\Gamma ⊢\left({\pi }_{2}\left(⟨x,y⟩\right)\equiv y\right):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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:n\mathrm{Type}\phantom{\rule{2em}{0ex}}\Gamma ⊢z:A×B}{\Gamma ⊢\left(⟨{\pi }_{1}\left(z\right),{\pi }_{2}\left(z\right)⟩\equiv z\right):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, $×$ 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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,x:A,x\prime :A,y:B,y\prime :B⊢\left({\mathrm{hom}}_{A×B}\left(⟨x,y⟩,⟨x\prime ,y\prime ⟩\right)\equiv {\mathrm{hom}}_{A}\left(x,x\prime \right)×{\mathrm{hom}}_{B}\left(y,y\prime \right)\right):\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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,x:A,y:B⊢\left(⟨{1}_{x},{1}_{y}⟩\equiv {1}_{⟨x,y⟩}\right):{\mathrm{hom}}_{A×B}\left(⟨x,y⟩,⟨x,y⟩\right)}$\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}\phantom{\rule{2em}{0ex}}\Gamma ⊢B:\mathrm{Cat}}{\Gamma ,\begin{array}{c}x:A,x\prime :A,x″:A,f:{\mathrm{hom}}_{A}\left(x,x\prime \right),f\prime :{\mathrm{hom}}_{A}\left(x\prime ,x″\right),\\ y:B,y\prime :B,y″:B,g:{\mathrm{hom}}_{B}\left(y,y\prime \right),g\prime :{\mathrm{hom}}_{B}\left(y\prime ,y″\right)\end{array}⊢\left(⟨f\prime \circ f,g\prime \circ f⟩\equiv ⟨f\prime ,g\prime ⟩\circ ⟨f,g⟩\right):{\mathrm{hom}}_{A×B}\left(⟨x,y⟩,⟨x″,y″⟩\right)}$\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)}