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 : n Type ( unit type ) \frac{}{\vdash 1:n Type} (\text{unit type})
Strictly speaking, 1 1 should be decorated with an n n , 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 : n Type Γ ⊢ B : n Type Γ ⊢ A × B : n Type \frac{\Gamma \vdash A:n Type \qquad \Gamma \vdash B:n Type}
{\Gamma \vdash A\times B:n Type}
Γ ⊢ A : n Type Γ ⊢ B : n Type Γ ⊢ 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 : n Type Γ ⊢ B : n Type Γ ⊢ 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 : n Type Γ ⊢ B : n Type Γ ⊢ 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 : n Type Γ ⊢ B : n Type Γ ⊢ 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 : n Type Γ ⊢ B : n Type Γ ⊢ 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 : n Type Γ ⊢ B : n Type Γ ⊢ 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 y ⟩ ≡ 1 ⟨ 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 ″ ) ⊢ ( ⟨ f ′ ∘ f , g ′ ∘ f ⟩ ≡ ⟨ f ′ , g ′ ⟩ ∘ ⟨ f , 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 at 20:09:38.
See the history of this page for a list of all contributions to it.