[Agda] Yet another questions about equality

[Peter Hancock]

On 15/02/2011 17:04, Permjacov Evgeniy wrote:
> On 02/15/2011 07:25 PM, Andreas Abel wrote:
>
>>> 2) is it possible to prove
>>>     ∀ {ℓ : Level} {A B : Set ℓ} {f g : A → B} → (∀ (a : A) → f a ≡ g a) →
>>> f ≡ g
>>
>>
>> This is functional extensionality, which is not provable in Agda.
> What problem I will face if I postulate this proposition ?

For many of us, I guess, the attraction of type theory has been, in part,
that it makes computational sense. Broadly speaking.

The problem with postulating axioms is that, despite them being often/sometimes "reasonable",
in some philosophical sense, they are just constants that sit there, like stones, and mean nothing
computationally. They don't participate in calculation of values from
expressions from expressions, or in checking interconvertibility at type-checking
time.  They're fossils.

So, if you postulate this principle, as far as I know, nothing bad or
good will happen.  The problem is that nothing will *happen*.
(Unless, you have an idea about how to make it participate in actual computation.)

Hank
(Sorry if this appears unthreaded.  I'm no good with computers, and
sent it only to Permjacov.)