Not signed in

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

Site Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Mathematics, Physics & Philosophy: Predicates and Equivalences

Bottom of Page

1 to 5 of 5

- CommentRowNumber1.
- CommentAuthorNima
- CommentTimeAug 11th 2021
- (edited Aug 11th 2021)
- PermaLink
Author: Nima
Format: MarkdownItexI 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?

I think I’m missing something here.

Say we have an equivalence

$<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>A</mi><mo>≃</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">A \simeq B</annotation></semantics></math>$

and a polymorphic predicate:

$<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo>:</mo><msub><mi>Π</mi> <mrow><mi>A</mi><mo>:</mo><mi>U</mi></mrow></msub><mi>A</mi><mo>→</mo><mi>U</mi></mrow><annotation encoding="application/x-tex">P : \Pi_{A:U} A \rightarrow U</annotation></semantics></math>$

Then should we not expect the following equivalence?

$<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>Σ</mi> <mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow></msub><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><mo>≃</mo><msub><mi>Σ</mi> <mrow><mi>b</mi><mo>:</mo><mi>B</mi></mrow></msub><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></mrow><annotation encoding="application/x-tex">\Sigma_{a:A} {P (A, a)} \simeq \Sigma_{b:B} {P (B, b)}</annotation></semantics></math>$

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)
- PermaLink
Author: David_Corfield
Format: MarkdownItexSo 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 given an equivalence $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>≃</mo><mi>B</mi></mrow><annotation encoding="application/x-tex">f: A \simeq B</annotation></semantics></math>$ , does it induce an equivalence $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>Σ</mi> <mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow></msub><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo>,</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><mo>≃</mo><msub><mi>Σ</mi> <mrow><mi>b</mi><mo>:</mo><mi>B</mi></mrow></msub><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo>,</mo><mi>b</mi><mo stretchy="false">)</mo></mrow></mrow><annotation encoding="application/x-tex">\Sigma_{a:A} {P (A, a)} \simeq \Sigma_{b:B} {P (B, b)}</annotation></semantics></math>$ ?

Doesn’t this concern that dependent map of Lemma 2.3.4 of the HoTT book? In the terms here:
$<math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><msub><mi>apd</mi> <mi>P</mi></msub><mo>:</mo><munder><mo lspace="0.16667em" rspace="0.16667em">∏</mo> <mrow><mi>f</mi><mo>:</mo><mi>A</mi><mo>=</mo><mi>B</mi></mrow></munder><mo stretchy="false">(</mo><msub><mi>f</mi> <mo>*</mo></msub><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><msub><mo>=</mo> <mrow><mi>B</mi><mo>→</mo><mi>U</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>.</mo></mrow><annotation encoding="application/x-tex"> apd_P: \prod_{f:A =B}(f_{\ast} P(A) =_{B \to U} P(B)). </annotation></semantics></math>$
- CommentRowNumber3.
- CommentAuthorDavid_Corfield
- CommentTimeAug 12th 2021
- PermaLink
Author: David_Corfield
Format: MarkdownItexSo you have equivalences between $P(A)(a)$ and $f_\ast P(A)(f(a))$ and $P(B)(f(a))$.

So you have equivalences between $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(A)(a)</annotation></semantics></math>$ and $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mi>f</mi> <mo>*</mo></msub><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">f_\ast P(A)(f(a))</annotation></semantics></math>$ and $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(B)(f(a))</annotation></semantics></math>$ .
- CommentRowNumber4.
- CommentAuthorUlrik
- CommentTimeAug 12th 2021
- PermaLink
Author: Ulrik
Format: MarkdownItexYes, 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.

Yes, it follows that $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo>∘</mo><mi>f</mi><msub><mo>=</mo> <mrow><mi>A</mi><mo>→</mo><mi>U</mi></mrow></msub><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(B) \circ f =_{A \to U} P(A)</annotation></semantics></math>$ (transporting on the other side) and hence for every $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>a</mi><mo>:</mo><mi>A</mi></mrow><annotation encoding="application/x-tex">a : A</annotation></semantics></math>$ , $<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi>P</mi><mo stretchy="false">(</mo><mi>B</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>f</mi><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo><mo stretchy="false">)</mo><mo>≃</mo><mi>P</mi><mo stretchy="false">(</mo><mi>A</mi><mo stretchy="false">)</mo><mo stretchy="false">(</mo><mi>a</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">P(B)(f(a)) \simeq P(A)(a)</annotation></semantics></math>$ . This in turn induces the desired equivalence.
- CommentRowNumber5.
- CommentAuthorNima
- CommentTimeAug 15th 2021
- PermaLink
Author: Nima
Format: MarkdownItexThanks David and Ulrik. I think I follow.

Thanks David and Ulrik. I think I follow.

1 to 5 of 5

nForum

Discussion Feed

Not signed in

Site Tag Cloud

Atrium > Mathematics, Physics & Philosophy: Predicates and Equivalences