Dan Krejsa

2018-03-26 23:15:47 UTC

Hi,

If â¥ is the prototypical empty type, is it possible in Agda to prove

fromâ¥uniq : â {i} {A : Set i} (f g : â¥ -> A) -> f â¡ g

(where â¡ is propositional equality) without assuming extra postulates

such as functional extensionality?

My instinct is to doubt it, but the emptiness of the domain gives me

pause...

- Dan

If â¥ is the prototypical empty type, is it possible in Agda to prove

fromâ¥uniq : â {i} {A : Set i} (f g : â¥ -> A) -> f â¡ g

(where â¡ is propositional equality) without assuming extra postulates

such as functional extensionality?

My instinct is to doubt it, but the emptiness of the domain gives me

pause...

- Dan