The principle of weak function extensionality states that the dependent product type of a family of contractible types is itself contractible.
This is equivalent to the condition that the dependent product type of a family of h-propositions itself is an h-proposition:
Weak function extensionality is not equivalent to the principle of unique choice. The principle of unique choice states that the dependent product type of a family of contractible types is pointed