The principle of unique choice (aka function comprehension) is the idea that total functional relations and functions correspond precisely.
In HOL this principle can be written as follows: for any types and ,
The quantifier is interpreted as "there exists a unique element". Thus, if we have for every a unique choice of such that , then this choice can be bootstrapped into a function .
The principle of unique choice is "familiar from topos theory." Any leads on that?