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

[Dan Licata <d...@cs.cmu.edu>]

Hi Andy,

Thanks for the interesting comments!  A few replies below.  

>> In particular, based on Martin’s observation https://github.com/HoTT/book/issues/718#issuecomment-65378867
>> that any retraction of an identity type is an equivalence:
>> 
>>   retract-of-Id-is-Id : ∀ {A : Set} {R : A → A → Set} →
>>                       (r : {x y : A} → x == y -> R x y)
>>                       (s : {x y : A} → R x y → x == y)
>>                       (comp1 : {x y : A} (c : R x y) → r (s c) == c)
>>                       → {x y : A} → IsEquiv {x == y} {R x y} (r {x}{y})
>> 
>> it is enough to assert “ua” (equivalence to path) and the “beta” direction of the full univalence axiom, i.e. the fact that transporting along such a path is the equivalence:
>> 
>>   ua : ∀ {A B} → Equiv A B → A == B
>>   uaβ : ∀ {A B} (e : Equiv A B) → transport (\ X -> X) (ua e) == fst e
>> 
>> The “eta” direction comes for free by Martin’s argument.
> 
> You are stating this for the usual inductively defined Martin-Lof
> identity type ==, right?  

Yes. 

> 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.  

-Dan