Re: [HoTT] weak univalence with "beta" implies full univalence

[Andrew Pitts <Andrew...@cl.cam.ac.uk>]

On 7 September 2016 at 23:20, Dan Licata <d...@cs.cmu.edu> wrote:
>> Also I think you need to assume the identity types,
>> whatever they are, satisfy function extensionality don't you?
>
> I didn’t, but I stated uaβ as an equation at function type.  If it were pointwise, then I would have needed it.  For an identity type with definitional J-on-refl reduction, this suffices to get the usual statement of univalence (I updated the file a little to remove a use a funext to make sure).  Maybe this depends on having definitional J-on-refl though.

OK, I see. The proof I made up for myself used along the way the fact
that being contractible is a mere proposition; and for that I seemed
to need function extensionality. But in any case, stating uaβ
pointwise seems more useful. Plus the fact that in the models where we
have been using this nice characterisation of univalence, function
extensionality holds for the propositional identity types in question
for other reasons to do with them being given by paths, as you know.

Best wishes,

Andy