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

Z is a set #207

Closed
mortberg opened this issue Aug 8, 2018 · 4 comments · Fixed by #245
Closed

Z is a set #207

mortberg opened this issue Aug 8, 2018 · 4 comments · Fixed by #245
Assignees
Labels

Comments

@mortberg
Copy link
Collaborator

mortberg commented Aug 8, 2018

When trying out my problem we will need a proof that the integers form a set. We can either prove this directly using J or using Hedberg. Having both proofs could be interesting just to compare for efficiency.

For proofs in cubicaltt/hcomptrans see setZ' (using J) and ZSet (using Hedberg) in: https://github.com/mortberg/cubicaltt/blob/pi4s3/examples/brunerie2.ctt

@ecavallo
Copy link
Collaborator

ecavallo commented Aug 9, 2018

I'll give this a shot.

@ecavallo ecavallo self-assigned this Aug 9, 2018
@ecavallo
Copy link
Collaborator

@jonsterling I've coded up a proof using Hedberg, shall I wait on #230 or...?

@jonsterling
Copy link
Collaborator

@ecavallo Oh cool!!! Can you commit the proof directly to the Rectification Campaign branch? I will merge soon, but I just want to clean up a few minor things.

@jonsterling
Copy link
Collaborator

@ecavallo OK, I ended up merging that branch, so feel free to put your code on a new branch, based on master.

@ecavallo ecavallo mentioned this issue Aug 17, 2018
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.

3 participants