How to prove that equal function types have equal domains?

Question

I want to prove

∀ {ℓ} {A B C D : Set ℓ} → (A → B) ≡ (C → D) → A ≡ C

(and similar for the codomain).

If I had a function domain that returns the domain of a function type, I could write the proof as

cong domain

but I don't think it's possible to write such a function.

Is there any way to do this?

Answer 1

I posed a very similar question on the Agda mailing list a few months ago, see: http://permalink.gmane.org/gmane.comp.lang.agda/5624. The short answer is that you cannot prove this in Agda.

The technical reason is that the unification algorithm used internally by Agda for pattern matching doesn't include a case for problems of the form (A → B) ≡ (C → D), so this definition does not typecheck:

cong-domain : ∀ {ℓ} {A B C D : Set ℓ} → (A → B) ≡ (C → D) → A ≡ C
cong-domain refl = refl

It is also impossible to define the function domain directly. Think about it: what should be the domain of a type that is not a function type, e.g. Bool?

The deeper reason why you cannot prove this is that it would be incompatible with the univalence axiom from Homotopy Type Theory. In an answer given by Guillaume Brunerie on my mail, he gives the following example: Consider the two types Bool -> Bool and Unit -> (Bool + Bool). Both have 4 elements, so we can use the univalence axiom to give a proof of type Bool -> Bool ≡ Unit -> (Bool + Bool) (in fact there are 24 different proofs). But clearly we do not want Bool ≡ Unit! So in the presence of univalence, we cannot assume that equal function types have equal domains.

In the end, I 'solved' this problem by passing an extra argument of type A ≡ C everywhere it was needed. I know it's not ideal, but maybe you can do the same.

I should also note that Agda does include an option for injective type constructors, which you can enable by putting {-# OPTIONS --injective-type-constructors #-} at the top of your .agda file. This allows you for example to prove A ≡ B from List A ≡ List B, but unfortunately this only works for type constructors such as List, and not for function types.

You could of course always make a feature request at https://code.google.com/p/agda/issues/list to add a option --injective-function-types to Agda. This option would be incompatible with univalence, but so is --injective-type-constructors, yet for many applications this is not a real problem. I feel that the main Agda developers are usually very open to such requests, and very fast to add them to the development version of Agda.