Empty function

Stream: Is there code for X?

[Will Fourie]

Assume I have types A, B as well as functions f, g : A -> B and a proof of H : is_empty A.

How can I show that f must equal g?

Set theoretically I would just say that f and g must both be equal to the empty function and so are equal to each other. I don’t know if that still works in type theory.

[Andrew Yang]

docs#funext and then docs#is_empty.elim.
Not sure if there is a one lemma solution.

[Will Fourie]

Turns out that

subsingleton.elim f g works

[Will Fourie]

^ keeping this here for reference