The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Oh, right, I suppose it's provable that (~ notT A -> ~ notT B) -> ~
notT (A -> B).  It's (inhabited A -> inhabited B) -> inhabited (A ->
B) that's probably not provable.

Indeed it does not seem provable. If we allow ourselves to see [inhabited A] as something like the set [A] quotiented by the total relation (a legitimate view in an arbitrary topos, so in set theory), then we can first remark that [inhabited] is a monad, so that [inhabited A -> inhabited B] is equivalent to [A -> inhabited B] (but not isomorphic!). So it suffices to think about [(A->inhabited B)->inhabited(A->B)].

We can start to see why this is not realistic : if [A] is the quotient of some set [A₀], then by the universal property of quotients any function in [A₀ -> B] is a function [A->inhabited B], but there is no general way of deducing a function [A->B] from such a function. Unless, that is, we can "choose" a canonical element in each equivalence class in [A] (or we use the excluded middle to find a completely different one). And indeed, this principle is a weak form of choice, here is one statement of (internal, I think) choice: [(Π(x:A), inhabited B) -> inhabited(Π(x:A),B)] (in words: an arbitrary product of inhabited sets is inhabited).