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

Generate a proof of adjunction #57

Closed
tlringer opened this issue Jun 12, 2019 · 4 comments
Closed

Generate a proof of adjunction #57

tlringer opened this issue Jun 12, 2019 · 4 comments
Assignees
@nateyazdani
Labels
enhancement New feature or request

Comments

@tlringer
Copy link
Collaborator

See #39
@tlringer tlringer added the enhancement New feature or request label Jun 12, 2019
@tlringer
Copy link
Collaborator Author

Useful: https://github.com/CoqHott/univalent_parametricity/blob/master/theories/HoTT.v

@nateyazdani nateyazdani self-assigned this Jun 14, 2019
@tlringer tlringer mentioned this issue Jun 19, 2019
Open
@tlringer
Copy link
Collaborator Author

tlringer commented Jul 3, 2019

This should quantify over all section/retraction proofs

@tlringer tlringer mentioned this issue Jul 3, 2019
Closed
@tlringer
Copy link
Collaborator Author

tlringer commented Aug 29, 2019 •
edited
Loading

We can use this: https://github.com/jashug/IWTypes/blob/master/Adjointification.v

We should obviously credit Jasper everywhere we do

@nateyazdani nateyazdani mentioned this issue Sep 6, 2019
Merged
@nateyazdani
Copy link
Contributor

Resolved by #68.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nateyazdani nateyazdani

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nateyazdani @tlringer