Re: [HoTT] Voevodsky on formalizing type theory

[Martin Escardo]

On 13/07/15 21:34, Michael Shulman wrote:
> On Mon, Jul 13, 2015 at 1:18 PM, N. Raghavendra <ra...@hri.res.in> wrote:
>> In usual mathematics, the notation x |--> x^2 : N --> N does not "mean"
>> an operation that does something to its input. It "means" a set of
>> ordered pairs with some properties. Does the notation
>> \lambda(x:N).x^2 : N --> N in type theory also "mean" that same thing?
>
> In usual mathematics, the notation x |--> x^2 means a function. It is
> a peculiarity of set theoretic foundations that a "function" is
> defined to be a set of ordered pairs with some properties. It is not
> true in type-theoretic foundations that a function is a set of ordered
> pairs. However, a function is still a mathematical object, on the
> same ontological level as a set of ordered pairs, which is denoted by
> the equivalent syntaxes x |--> x^2 or \lambda(x:N).x^2.

I would like to add something to this discussion.

In set theory, we also have some functions like those of type theory,
namely the propositional functions. Two of them are "\in" (the
membership relation) and "=", which are truth-valued functions.

They are not defined as graphs in ZFC. (Think why!)

There is no problem in defining a function to be a type of ordered
pairs in type theory.

Define unique existence in type theory by

Exists!(x:X).A(x) = isContractible(Sigma(x:X).A(x)).

(So, not only is the x:X is unique, but also the witness of A(x).
Which is automatic if A(x) is a proposition.)

This type Exists!(x:X).A(x) is a proposition or truth value (any two
of its points are equal).

We have an equivalence

(X->Y) ~ Sigma(R:X->Y->U).Pi(x:X).Exists!(y:Y). R x y.

(I think this is in Egbert Rijke's masterw thesis, but in any case it
is easy to check.)

The relation R collects the ordered pairs (x,y), and the proposition
Pi(x:X).Exists!(y:Y). R x y says that this collection of ordered pairs
is functional.

It is obtained by R x y = (fx = y) for any given f:X->Y, of
course. Or, conversely, we recover f(x) using the witness of
Pi(x:X).Exists!(y:Y). R x y.

So also in type theory, in the presence of univalence
(=extensionality) a function *is* a functional binary relation.

But, of course, like in set theory, at some point we need a primitive
notion of function not coded as a set of ordered pairs. Here it is
manifested as the characteristic function R:X->Y->U of the collection
of ordered pairs.

If we take the type of such pairs, namely,
Sigma(x:X).Sigma(y:Y).f(x)=y, we get a type equivalent, and hence
equal, to X. But it is also the case, in set theory, that the graph of
any function X->Y is isomorphic to X. Here, however, we cannot recover
f from Sigma(x:X).Sigma(y:Y).f(x)=y, although we can recover it from
its graph R x y = (f(x)=y) *and* the witness of functionality of R.

Martin