Is the univalence axiom injective?
Is the univalence axiom invertible (modulo paths)? Is it possible to prove, using Agda's Cubical library, to prove the following:
open import Cubical.Core.Glue
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} →
ua f ≡ ua g → equivFun f ≡ equivFun g
I suspect the above should hold, because in example 3.19 of the HoTT book, there is a step in the proof where an equivalence between two equivalences is used to prove the equivalence between their functions:
[...] so
fis an
equivalence. Hence, by univalence,fgives rise to a pathp : A ≡ A.
If
pwere equal torefl A, then (again by univalence)fwould equal the
identity function ofA.
agda cubical-type-theory homotopy-type-theory
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
add a comment |
Is the univalence axiom invertible (modulo paths)? Is it possible to prove, using Agda's Cubical library, to prove the following:
open import Cubical.Core.Glue
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} →
ua f ≡ ua g → equivFun f ≡ equivFun g
I suspect the above should hold, because in example 3.19 of the HoTT book, there is a step in the proof where an equivalence between two equivalences is used to prove the equivalence between their functions:
[...] so
fis an
equivalence. Hence, by univalence,fgives rise to a pathp : A ≡ A.
If
pwere equal torefl A, then (again by univalence)fwould equal the
identity function ofA.
agda cubical-type-theory homotopy-type-theory
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
add a comment |
Is the univalence axiom invertible (modulo paths)? Is it possible to prove, using Agda's Cubical library, to prove the following:
open import Cubical.Core.Glue
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} →
ua f ≡ ua g → equivFun f ≡ equivFun g
I suspect the above should hold, because in example 3.19 of the HoTT book, there is a step in the proof where an equivalence between two equivalences is used to prove the equivalence between their functions:
[...] so
fis an
equivalence. Hence, by univalence,fgives rise to a pathp : A ≡ A.
If
pwere equal torefl A, then (again by univalence)fwould equal the
identity function ofA.
agda cubical-type-theory homotopy-type-theory
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
Is the univalence axiom invertible (modulo paths)? Is it possible to prove, using Agda's Cubical library, to prove the following:
open import Cubical.Core.Glue
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} →
ua f ≡ ua g → equivFun f ≡ equivFun g
I suspect the above should hold, because in example 3.19 of the HoTT book, there is a step in the proof where an equivalence between two equivalences is used to prove the equivalence between their functions:
[...] so
fis an
equivalence. Hence, by univalence,fgives rise to a pathp : A ≡ A.
If
pwere equal torefl A, then (again by univalence)fwould equal the
identity function ofA.
agda cubical-type-theory homotopy-type-theory
agda cubical-type-theory homotopy-type-theory
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
asked Nov 14 '18 at 14:27
CactusCactus
18.8k848113
18.8k848113
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
add a comment |
To put András's answer into code, we can prove injectivity of equivalency functions in general:
equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) →
∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
x , refl ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
equivCtr f (equivFun f x) ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
x′ , p ∎
and then given
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
we get
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g
The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.
UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53302504%2fis-the-univalence-axiom-injective%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
add a comment |
Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
add a comment |
Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
Sure, ua is an equivalence, so it's injective. In the HoTT book, the inverse of ua is idtoeqv, so by congruence idtoeqv (ua f) ≡ idtoeqv (ua g) and then by inverses f ≡ g. I'm not familiar with the contents of cubical Agda prelude but this should be provable since it follows directly from the statement of univalence.
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
edited Nov 14 '18 at 15:16
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
answered Nov 14 '18 at 15:11
András KovácsAndrás Kovács
25.1k33782
25.1k33782
add a comment |
add a comment |
To put András's answer into code, we can prove injectivity of equivalency functions in general:
equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) →
∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
x , refl ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
equivCtr f (equivFun f x) ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
x′ , p ∎
and then given
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
we get
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g
The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.
UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
add a comment |
To put András's answer into code, we can prove injectivity of equivalency functions in general:
equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) →
∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
x , refl ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
equivCtr f (equivFun f x) ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
x′ , p ∎
and then given
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
we get
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g
The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.
UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
add a comment |
To put András's answer into code, we can prove injectivity of equivalency functions in general:
equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) →
∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
x , refl ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
equivCtr f (equivFun f x) ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
x′ , p ∎
and then given
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
we get
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g
The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.
UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
To put András's answer into code, we can prove injectivity of equivalency functions in general:
equivInj : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A ≃ B) →
∀ x x′ → equivFun f x ≡ equivFun f x′ → x ≡ x′
equivInj f x x′ p = cong fst $ begin
x , refl ≡⟨ sym (equivCtrPath f (equivFun f x) (x , refl)) ⟩
equivCtr f (equivFun f x) ≡⟨ equivCtrPath f (equivFun f x) (x′ , p) ⟩
x′ , p ∎
and then given
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
we get
uaInj : ∀ {ℓ} {A B : Set ℓ} {f g : A ≃ B} → ua f ≡ ua g → equivFun f ≡ equivFun g
uaInj {f = f} {g = g} = cong equivFun ∘ equivInj (invEquiv univalence) f g
The only problem is, univalence is not readily available in the Cubical library. Hopefully that is getting sorted out shortly.
UPDATE: In reaction to the above bug ticket, proof of univalence is now available in the Cubical library.
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
edited Nov 22 '18 at 6:06
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
answered Nov 16 '18 at 13:24
CactusCactus
18.8k848113
18.8k848113
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53302504%2fis-the-univalence-axiom-injective%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
