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.

Sign up for GitHub

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

Jump to bottom

Write out the definion of Coxeter relation as a HIT #8

Closed
vikraman opened this issue Dec 21, 2020 · 1 comment · Fixed by #32
Closed

Write out the definion of Coxeter relation as a HIT #8

vikraman opened this issue Dec 21, 2020 · 1 comment · Fixed by #32
Assignees
@vikraman @inexxt
Labels
definition FSMG Pi
Projects
Pi+

Comments

@vikraman
Copy link
Owner

No description provided.

@vikraman vikraman created this issue from a note in Pi+ (To do) Dec 21, 2020
@vikraman vikraman moved this from To do to In progress in Pi+ Dec 21, 2020
@inexxt
Copy link
Collaborator

inexxt commented Dec 23, 2020

There is already a definition in Pi+/Coxeter/Coxeter.agda, but we need another form, as a HIT.

@vikraman vikraman changed the title Write out the definion of Coxeter relation Write out the definion of Coxeter relation as a HIT Dec 23, 2020
@vikraman vikraman mentioned this issue Jan 2, 2021
Merged
Pi+ automation moved this from In progress to Done Jan 6, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@vikraman vikraman

@inexxt inexxt

Labels
definition FSMG Pi
Projects
Pi+
Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Define Sn as a HIT vikraman/2DTypes
2 participants
@vikraman @inexxt