Comment about type theory in Lawvere and Rosebrugh's Sets for Mathematics

116 Views Asked by At

The Foreword to Sets for Mathematics (second section, titled Organization) contains the following comment, about the differences between ETCS and other foundations of mathematics:

Each map needs both an explicit domain and an explicit codomain (not just a domain, as in previous formulations of set theory, and not just a codomain, as in type theory).

I understand the remark about set theory: a function as a set of ordered pairs determines its domain but not its codomain.

But what do the authors mean when they say a function in type theory has an explicit codomain but not an explicit domain?

A term of the simple type $A \rightarrow B$ has both an explicit domain and codomain. A term of a dependent type $\Pi x:A.B(x)$ arguably has an explicit domain but not a codomain (since its codomain would need to be something like $\bigcup x:A.B(x)$, which does not exist as a type in Martin-Löf Type Theory).

1

There are 1 best solutions below

0
On

I believe the point is that a term $x:A$ of type theory is interpreted categorically as an arbitrary morphism into $A$.