I can't remember if I've read this somewhere, but it is tempting to assume that ⊥ is an initial object. But then it must be possible to construct proofs based on the uniqueness of the ⊥-elim arrows.
Like this:
false-elim : forall {A : Set} -> False -> A
false-elim ()
false-iso : forall {A B : Set} -> (g : A -> False)
-> (f : A -> B) -> f == (f o false-elim o g)
That is, if there is an arrow from A into ⊥, then A is isomorphic to ⊥. Ok, if the assumption that (A -> ⊥) is an isomorphism is wrong, at least must be possible to show the uniqueness of ⊥-elim:
false-elim-uniq : forall {A B : Set} -> (f : A -> B)
-> false-elim == (f o false-elim)
But this is not obvious, too. So, is ⊥-elim meant to be unique in (flavour of) intuitionistic type theory (Agda is based on)?
It is possible to construct the proof if an element of A can be constructed:
false-iso : forall {A B : Set} -> (g : A -> False)
-> (f : A -> B) -> A -> f == (f o false-elim o g)
But that's not quite the same statement. It does say I can prove homotopy of the said functions (and show A ≅ ⊥).
Given it some thought, I guess I can narrow down my problem to: if all I can show is a homotopy f ~ (f o false-elim o g), what does the universal property of false-elim look like?