[Agda] dependent extensionality

[Thorsten Altenkirch]

On 26 Sep 2010, at 13:10, David Leduc wrote:

> Hi,
> 
> Is it safe to add the following postulate in Agda?
> 
>  postulate extensionality : {l1 l2 : Level}{A : Set l1}{B : A -> Set
> l2}{f g : (a : A) -> B a} -> (∀ x → f x ≡ g x) → f ≡ g

Yes, it should be. I think dependent extensionality and non-dependent extensionality are equivalent anyway and I don't see how the levels should cause any harm.

Thorsten

> 
> P.S. Note that the definition of Extensionality in
> Relation.Binary.PropositionalEquality is not dependent, and forces
> domain and codomain to be at the same level. Maybe it should be
> generalized as above.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda