Hm, the two types are not provably isomorphic... Ok, this is a tricky 
question indeed!

On Monday, September 12, 2016 at 11:55:45 AM UTC+2, Andrew Polonsky wrote:
>
> > I suspect "one of them provably has but the other doesn't" should mean 
> "one 
> > of them provably has but the other provably does not have". 
>
> Type theory with reflection rule usually contains the rule equating 
> all proofs of equality: 
>
>        p : Id(A;x,y) 
> --------------------------- 
>   p == refl : Id(A;x,y) 
>
> If this is admitted, then the following modified example works: 
>
> A = Id(U;Bool,Bool) 
> B = Iso(Bool,Bool) 
> P(X) = Id(U;A,X) 
>
> Clearly, P(A).  Suppose P(B).  By equality reflection, A == B : U. 
> But then, for x : Iso(Bool,Bool), we have x : Id(U;Bool,Bool), whence x == 
> refl. 
> Since this holds for arbitrary x, we have x==y for arbitrary x,y : 
> Iso(Bool,Bool), a contradiction. 
>
> Generally, I think any proof that equality reflection is inconsistent 
> with univalence could be adapted to yield a counterexample as above. 
>
> Cheers, 
> Andrew 
>