[Agda] Yet another questions about equality

[Andreas Abel]

Dear Evgeniy,

On 2/15/11 4:55 PM, Permjacov Evgeniy wrote:
>
> 1) Let assume
>
> infixr 1 _⊎_
>
> data _⊎_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
>    inj₁ : (x : A) → A ⊎ B
>    inj₂ : (y : B) → A ⊎ B
>
> sum : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Set ℓ₁} {B : Set ℓ₂} {R : A ⊎ B → Set ℓ₃ }
>      → ( (x : A) → R (inj₁ x) )
>      → ( (y : B) → R (inj₂ y) )
>      → (x : A ⊎ B ) → R x
> sum c₁ c₂ (inj₁ l) = c₁ l
> sum c₁ c₂ (inj₂ r) = c₂ r
>
>
> how to prove
>    sum inj₁ inj₂  ≡ id ?
>
> 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.

For the same reason, 1) is not provable.

Leibniz equality \equiv is intensional, so functions can be different 
even if they behave the same on all arguments.  [This is not so 
unnatural, e.g., quick sort and insertion sort have the same 
observational behavior, they both sort, but they are still different 
functions.]

Maybe you want extensional equality, this can be done in general using 
setoids.

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/