Michael Shulman
dependent types in a 2-category

This is just bits and pieces for now; something more coherent will come later.

Overview

Of course, we should be able to treat an nn-type as an mm-type for any mnm\ge n. When n=1n=-1 and m=0m=0 this corresponds to replacing a proposition φ\varphi by the set {*|φ}\{ * | \varphi\}, while when n=0n=0 and m=1m=1 it corresponds to treating a set as a discrete category. It should also be true that the resulting mm-type is appropriately truncated.

Type-raising

The following operations allow us to interpret an nn-type as an mm-type whenever mnm\ge n.

ΓA:nTypeΓ|A|:(n+1)Type(n=0,1)\frac{\Gamma \vdash A:n Type} {\Gamma\vdash {|A|}:(n+1) Type} (n = 0,-1)

ΓA:nTypeΓ,x:Ai n(x):|A|(n=0,1)\frac{\Gamma \vdash A:n Type} {\Gamma, x:A \vdash i_n(x) : {|A|}} (n = 0,-1)

ΓA:nTypeΓ,x:|A|j n(x):A(n=0,1)\frac{\Gamma \vdash A:n Type} {\Gamma, x:{|A|} \vdash j_n(x) : A} (n = 0,-1)

ΓA:nTypeΓ,x:Axj n(i n(x)):A(n=0,1)\frac{\Gamma \vdash A:n Type} {\Gamma, x:A \vdash x\equiv j_n(i_n(x)) : A} (n = 0,-1)

ΓA:nTypeΓ,x:|A|xi n(j n(x)):|A|(n=0,1)\frac{\Gamma \vdash A:n Type} {\Gamma, x:{|A|} \vdash x\equiv i_n(j_n(x)) : {|A|}} (n = 0,-1)

It follows that if φ:Prop\varphi:Prop, then x:|φ|,y:|φ|xyx:{|\varphi|}, y:{|\varphi|} \vdash x\equiv y, since j 1(x)j 1(y)j_{-1}(x)\equiv j_{-1}(y) as both are terms of a (1)(-1)-type φ\varphi. Thus, |φ|{|\varphi|} is in fact a subsingleton as desired. What remains to assert is that if A:SetA:Set then |A|:Cat{|A|}:Cat is a discrete category.

ΓA:SetΓ,x:|A|,y:|A|,f:hom |A|(x,y)(xy)\frac{\Gamma \vdash A:Set} {\Gamma, x:{|A|}, y:{|A|}, f:hom_{|A|}(x,y) \vdash (x \equiv y)}

ΓA:SetΓ,x:|A|,f:hom |A|(x,x)(f1 x)\frac{\Gamma \vdash A:Set} {\Gamma, x:{|A|}, f:hom_{|A|}(x,x) \vdash (f \equiv 1_x)}

Dependent sums

In theory, the ways to type the formation of dependent sums Σ x:AB(x)\Sigma_{x:A} B(x) are parametrized by three sorts: the sort of AA, the sort of BB, and the sort of the result. In our case, we allow two general classes of dependent sums.

  • In the first, BB must be a proposition, while AA can be anything, and in this case the result is a proposition. This construction gives existential quantifiers, so we will notate it as (x:A)B(x)(\exists x:A) B(x).
  • In the second, AA must be a set, while BB can be anything, and the result has the same sort as BB. This construction gives “indexed disjoint unions,” and we will use the ordinary dependent sum notation Σ x:AB(x)\Sigma_{x:A} B(x) for it.

Note that in the overlap case when AA is a set and BB is a proposition, we get two different ways to form a dependent sum Σ x:AB(x)\Sigma_{x:A} B(x) depending on what the result type is. If the result is a proposition, then it is the proposition (x:A)B(x)(\exists x:A) B(x), while if the result is a set, then it is the set {x:A|B(x)}\{x:A | B(x) \}. The difference from a computational point of view is that in the second case, it is possible to extract the witness x:Ax:A, while in the first it is not.

There should also be dependent sums of the second sort where AA is a category, with the result being a category. However, in this case, unless the dependence of BB on AA is given functorially, then it is not possible to determine the morphisms in the dependent sum. We will study the general case of functorially dependent types elsewhere, but here we do need one particular case.

Strong dependent sums

ΓA:SetΓ,x:AB(x):nTypeΓΣ x:AB(x):nType\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{ \Gamma \vdash \Sigma_{x:A}B(x) :n Type}

ΓA:SetΓ,x:AB(x):nTypeΓ,x:A,y:B(x)x,y:Σ x:AB(x)\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type}{\Gamma, x:A, y:B(x) \vdash \langle x,y\rangle : \Sigma_{x:A} B(x)}

ΓA:SetΓ,x:AB(x):nTypeΓ,z:Σ x:AB(x)π 1(z):A\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash \pi_1(z) :A}

ΓA:SetΓ,x:AB(x):nTypeΓ,z:Σ x:AB(x)π 2(z):B(π 1(x))\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash \pi_2(z) :B(\pi_1(x))}

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

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

ΓA:SetΓ,x:AB(x):nTypeΓ,z:Σ x:AB(x)zπ 1(z),π 2(z):Σ x:AB(x)\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):n Type} {\Gamma, z: \Sigma_{x:A}B(x) \vdash z \equiv \langle \pi_1(z), \pi_2(z)\rangle :\Sigma_{x:A}B(x)}

Note that when n=0n=0 and B(x)B(x) is independent of xx, then Σ x:AB(x)\Sigma_{x:A}B(x) is canonically isomomorphic to A×BA\times B. In ordinary type theory, one doesn’t need to define both binary products and dependent sums, since the former can be constructed from the latter in this way. However, since we aren’t allowing dependent sums over categories, we need binary products for categories given separately.

When n=1n=1 we also have rules for morphisms.

ΓA:SetΓ,x:AB(x):CatΓ,x:A,y 1:B(x),y 2:B(x),f:hom B(x)(y 1,y 2)x,f:hom Σ x:AB(x)(x,y 1,x,y 2)\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, x:A, y_1:B(x), y_2:B(x), f:hom_{B(x)}(y_1,y_2) \vdash \langle x,f\rangle : hom_{\Sigma_{x:A} B(x)}(\langle x,y_1\rangle, \langle x,y_2\rangle)}

ΓA:SetΓ,x:AB(x):CatΓ,z 1:Σ x:AB(x),z 2:Σ x:AB(x),f:hom Σ x:AB(x)(z 1,z 2)π 1(z 1)π 2(z 2):A\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash \pi_1(z_1)\equiv \pi_2(z_2): A}

ΓA:SetΓ,x:AB(x):CatΓ,z 1:Σ x:AB(x),z 2:Σ x:AB(x),f:hom Σ x:AB(x)(z 1,z 2)π 2(f):hom B(π 1(x))(π 2(z 1),π 2(z 2))\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash \pi_2(f): hom_{B(\pi_1(x))}(\pi_2(z_1),\pi_2(z_2))}

ΓA:SetΓ,x:AB(x):CatΓ,x:A,y 1:B(x),y 2:B(x),f:hom B(x)(y 1,y 2)fπ 2(x,f):hom B(x)(y 1,y 2)\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, x:A, y_1:B(x), y_2:B(x), f:hom_{B(x)}(y_1,y_2) \vdash f \equiv \pi_2(\langle x,f\rangle) : hom_{B(x)}(y_1,y_2)}

ΓA:SetΓ,x:AB(x):CatΓ,z 1:Σ x:AB(x),z 2:Σ x:AB(x),f:hom Σ x:AB(x)(z 1,z 2)fπ 1(z),π 2(f):hom Σ x:AB(x)(z 1,z 2)\frac{\Gamma \vdash A:Set \qquad \Gamma, x:A \vdash B(x):Cat} {\Gamma, z_1: \Sigma_{x:A}B(x), z_2 : \Sigma_{x:A}B(x), f:hom_{\Sigma_{x:A}B(x)}(z_1,z_2) \vdash f\equiv \langle \pi_1(z), \pi_2(f)\rangle: hom_{\Sigma_{x:A}B(x)}(z_1,z_2)}

Dependent products

As with dependent sums, in general the operation Π x:AB(x)\Pi_{x:A} B(x) is parametrized by the sorts of AA, of B(x)B(x), and of the result. Since exponentials in a 2-category require fibrations and variance, for now we restrict to the case when B(x)B(x) and Π x:AB(x)\Pi_{x:A} B(x) are both propositions. When AA is a set or a category, this gives universal quantification, which we write as (x:A)B(x)(\forall x:A) B(x), while when AA is also a proposition it gives implication, which we write as ABA\Rightarrow B.

Created on March 2, 2010 01:17:30 by Mike Shulman (75.3.151.132)