Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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?
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)).$So you have equivalences between $P(A)(a)$ and $f_\ast P(A)(f(a))$ and $P(B)(f(a))$.
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.
Thanks David and Ulrik. I think I follow.
1 to 5 of 5