Questions regarding univalence as generalized extensionality

[Martín Hötzel Escardó]

We know, thanks to Vladimir, that univalence implies both

 * FunExt: function extensionality (any two pointwise equal functions

   are equal)

and

 * PropExt: propositional extensionality (any two logically

   equivalent propositions are equal).

These implications hold in a basic intensional Martin-Löf type theory (just containing the ingredients needed to formulate them).

Thus, we may regard univalence as a generalized extensionality axiom for intensional Martin-Löf theories, as has been often emphasized.

Additionally, in informal parlance, we often see propositional extensionality equated with propositional univalence.

Let's clarify this, where we adopt X = Y as a notation for Id X Y:

 * PropExt (propositional extensionality): For all propositions P and Q, we have that

    (P → Q) and (Q → P) together imply P = Q.

 * PropUniv (propositional univalence): For all propositions P and Q, the map 

      idtoeq_{P,Q} : P = Q → P ≃ Q

   is an equivalence.

It is then clear that PropUniv → PropExt. However, the only way to get PropUniv from PropExt that I know of requires function extensionality as an additional assumption. Let's record this as

    - PropUniv → PropExt

    - FunExt → (PropExt → PropUniv).

 

Obvious question: does (PropExt→PropUniv) imply FunExt? I don't know.

Less obvious question: Does any of propositional univalence or propositional extensionality imply FunExt? That is, can we "linearize" the extensionality axioms as

   UA → PropUniv → PropExt → FunExt,

and, if not, less ambitiously as UA → PropUniv → FunExt?

Even less obvious: is univalence restricted to contractible types (call it ContrUniv) enough to get FunExt?

   UA → PropUniv → ContrUniv → FunExt?

Martin