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