[Agda] all functions have the same graph

[Martin Escardo]

This has probably already been observed by the HoTT aficionados, but I
thought it is sufficiently amusing to post it in this list, with Agda
code linked at the end.

Classical mathematics maintains that a function is the same thing as
its graph. Let's see what happens in type theory.

For f, g : X → Y, define

       graph f = Σ \x → Σ \y → f x ≡ y,

where "≡" of course is propositional equality (identity type). It may
be natural to suppose that, in intensional Martin-Löf theory,

   (*) graph f ≡ graph g → ∀(x : X) → f x ≡ g x.

However, one can show

   (**) univalence → ∀(f g : X → Y) → graph f ≡ graph g.

Because univalence is consistent, and (*) together with (**) proves an
inconsistency (all functions are pointwise equal), we conclude that (*)
is not provable in IMLTT.

Moreover, intensional MLTT cannot deny that all functions have the
same graph.

In particular, the statement "any two functions with equal graphs must
be equal" cannot be used to express extensionality in MLTT, because it
is provably false in IMLTT+univalence, which proves extensionality.

Here are the simple Agda proofs:

http://www.cs.bham.ac.uk/~mhe/papers/FunctionGraphsInIMLTT/FunctionGraphsInIMLTT.html

Anyway, if we want to confuse classical mathematicians, this seems to
be a really good approach: HoTT is compatible with excluded middle,
but still proves that all functions have the same graph.

Best,
Martin