[Agda] Yet another questions about equality

[Andreas Abel]

On 2/16/11 6:19 PM, Permjacov Evgeniy wrote:
> On 02/16/2011 07:44 PM, Andreas Abel wrote:
>
>> If you are happy to work with a closed set of types, for instance
>> 0,1,+,*,->, then you can define your own language of types (called a
>> universe) and define equality recursively on these types.
>>
> I'm afraid, I'll end with some sort of it. However, all I wish is to
> encode and prove properties of control structures. To do it, I need
> extensional (not intensional) equality. It even may lay in separate
> universe, but this feature is deprecated in agda. I do not need use of
> ext in typing, if something like this will raise, I can hand-build
> coercion function end this is enough for me. So, I'm currently consider
> either use of setoids, or hand-built equality type with term for ext.
>
> the problem is here
>
> data _≈_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ( [problem] suc ℓ
> [/problem] ) where
> int : x ≡ x → x ≈ x
> ext : (y : A) → (C D : Set ℓ) → ( teq : A ≡ (C → D)) → ( ∀ (c : C) →
> cast teq x c ≈ cast teq y c) → x ≈ y

This looks a bit weird.

The reason why _\sim_ lives in Set (suc l) is because the ext 
constructor quantifies over C : Set l.  Only in an impredicative 
universe, like Coq's Prop, you can quantify over C : Prop and still 
remain in Prop.

> Instead of getting Set \ell I got Set (suc \ell) . I have to understand
> this (what I'm currently cannot), and if it is OK, I'm satisfied with
> this equality relation, yet I'm searching literature about Setoids.
>
> BTW , I understand, that extensional equality leads to undecidable
> typechecking. However, why it is unacceptable to typecheck what can be
> typechecked intensionally and then build holes with what have to be
> proved by hand and check this proves?

There is a confusion of concepts.  The kind of extensional equality we 
are talking about here does not destroy decidability of type checking.

"Extentional type theory" with undecidable type checking refers to Nuprl 
and similar systems where the type checker considers two types equal if 
they are /provably/ equal.  Of course to decide this equality, the 
system would have to come up with a proof of equality, which is in 
general impossible.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/