[Agda] Yet another questions about equality

[Thorsten Altenkirch]

On 15 Feb 2011, at 11:25, Andreas Abel wrote:

> 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.

Indeed, two closed expressions are propositionally equal if and only if they are convertible. The reason is that if there is a proof of equality then because of normalisation there must be one in normal form. The only normal proof of an equality is refl and this forces both expressions to be convertible.

> 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.]

I think it is unnatural, since you cannot formulate an observation which distinguishes two extensionally equal functions. Hence all predicates preserve extesnional equality unless they refer to intensional equality.

Also, your problem 1 can be adressed if we add strong equality for coproducts to conversion which is known to be decidable. Hence changing definitional equality affects the propositions we can prove in Type Theory. This is strange since definitional equality is somehow arbitrary and changing it shouldn't affect the provable propositions.

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

I'd rather recommend to postulate ext. Setoids lead to an explosion of concepts since any operation on sets may have to be lifted to setoids.

There are ways to eliminate ext, this should end up in the implementation of Epigram one day (see our PLPV07 paper, if you are interested):
http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf
The basic idea is to define equality by recursion on types and then reconstruct subst and other constants. 

We did consider doing this for Agda but the required changes seemed quite substantial.

Cheers,
Thorsten


> 
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda