David Corfield dependent types

• $x: A \vdash B(x):Type$

Dependent sum

• $\vdash \sum_{x:A} B(x) : Type$

Terms are pairs $(a, p)$ where $a:A$ and $p: B(a)$. Can capture ‘The As which are B’ when $B(x)$ is a property.

Dependent product

• $\vdash \product_{x:A} B(x) : Type$

Terms are maps $f$ from $A$ such that $f(a) : B(a)$.

Philosophical issues

Material constitution

Much discussion has occurred about how one can say there is only one thing in cases where there are two descriptions, such as a statue and a lump of clay (see SEP: Material constitution).

The lump exists on Monday, but not yet the statue. It is worked on Tuesday into a statue. The statue doesn’t exist on Monday, while the lump of clay does. They must be different. Then does the sculptor hold two things after forming the statue.

Can we say that the type statue is a dependent sum – The lumps of clay which are formed for artistic effect (maybe this should be modified to allow statues of other substances).

Then a term of type Sculpture is a pair $(a, p)$ where $a: lump of clay$ and $p:Art(a)$ is a warrant that $a$ is formed for artistic effect.

When we say ‘X holds y’ we have X typed as person and y typed as object (space-time continuent). ‘X holds this statue’ means X holds the underlying object.

As with mathematical examples where the type theoretic reasoning carries with it proof terms, terms in ordinary language should do the same. If I say ‘this statue’, I should be prepared to answer the challenge ‘Why do you call it a statue?’ My term is being projected onto its second component, and I’m asked to construct something to fill that place.

Compare this to 2 as natural number, integer, rational, real, complex number.