Questions regarding univalence as generalized extensionality

Questions regarding univalence as generalized extensionality

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 1827 bytes --]

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


[-- Attachment #1.2: Type: text/html, Size: 2408 bytes --]