Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mistake in CayleyDickson.v #2149

Closed
Alizter opened this issue Dec 9, 2024 · 0 comments · Fixed by #2152
Closed

Mistake in CayleyDickson.v #2149

Alizter opened this issue Dec 9, 2024 · 0 comments · Fixed by #2152
Labels

Comments

@Alizter
Copy link
Collaborator

Alizter commented Dec 9, 2024

In CayleyDickson.v we mistakenly define conjugation on a suspension as:

Global Instance conjugate_susp (A : Type) `(Negate A)
: Conjugate (Susp A).
Proof.
srapply Susp_rec.
+ exact North.
+ exact South.
+ intro a.
exact (merid a).
Defined.

It should be merid (-a) rather than merid a.

This means that the H-space structure we get out of the Cayley-Dickson construction is incorrect.

@Alizter Alizter added the bug label Dec 9, 2024
Alizter added a commit to Alizter/HoTT that referenced this issue Dec 9, 2024
Signed-off-by: Ali Caglayan <[email protected]>

<!-- ps-id: 7c532112-95bc-4690-82c3-a579eeab1181 -->
@Alizter Alizter linked a pull request Dec 9, 2024 that will close this issue
Alizter added a commit that referenced this issue Dec 11, 2024
…and_fix__2149

cleanup in CayleyDickson and fix #2149
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant