Not signed in (Sign In)

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Sign in using OpenID

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorNima
• CommentTimeAug 11th 2021
• (edited Aug 11th 2021)

I think I’m missing something here.

Say we have an equivalence

$A \simeq B$

and a polymorphic predicate:

$P : \Pi_{A:U} A \rightarrow U$

Then should we not expect the following equivalence?

$\Sigma_{a:A} {P (A, a)} \simeq \Sigma_{b:B} {P (B, b)}$

It seems to me like this should be supported through substitute of like for like, but I can’t figure out how to prove this through the language of HoTT, even when using Univalence. Is my thinking correct here or am I missing something?

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeAug 12th 2021
• (edited Aug 12th 2021)

So given an equivalence $f: A \simeq B$, does it induce an equivalence $\Sigma_{a:A} {P (A, a)} \simeq \Sigma_{b:B} {P (B, b)}$?

Doesn’t this concern that dependent map of Lemma 2.3.4 of the HoTT book? In the terms here:

$apd_P: \prod_{f:A =B}(f_{\ast} P(A) =_{B \to U} P(B)).$
• CommentRowNumber3.
• CommentAuthorDavid_Corfield
• CommentTimeAug 12th 2021

So you have equivalences between $P(A)(a)$ and $f_\ast P(A)(f(a))$ and $P(B)(f(a))$.

• CommentRowNumber4.
• CommentAuthorUlrik
• CommentTimeAug 12th 2021

Yes, it follows that $P(B) \circ f =_{A \to U} P(A)$ (transporting on the other side) and hence for every $a : A$, $P(B)(f(a)) \simeq P(A)(a)$. This in turn induces the desired equivalence.

• CommentRowNumber5.
• CommentAuthorNima
• CommentTimeAug 15th 2021

Thanks David and Ulrik. I think I follow.