[Agda] Yet another questions about equality

[Permjacov Evgeniy]

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

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?