search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Formalize-yoneda-embedding-2 #103

Closed cesarbm03 closed 1 year ago

cesarbm03 commented 1 year ago

The proof of remak 9.4 as given in RS17. If this is correct, I can dualize and include the contravariant case.

emilyriehl commented 1 year ago

Hi @cesarbm03 does this PR overwrite the previous one? It seems like this one might make further edits on the definitions you've included there.

If so, maybe cancel that pull request (though you can first look at the comments I just left) and then we can review this one?

cesarbm03 commented 1 year ago

Yes, this one finishes the proof. I branched from formalize-yoneda, so I thought this one #103 would supersede #100 by default. I going to make the modifications to this pull request according to your comments on the previous one and cancel it afterwards. I just saw the issue on the style this afternoon, I was unaware of it until today. I'll be implementing from now on, so hopefully my submissions are cleaner.

emilyriehl commented 1 year ago

Okay, sounds good. Will you @ us when you're ready for review?

I'm not sure naming the terms "phi" after the name of the variable is best. Do others have suggestions for better names?

cesarbm03 commented 1 year ago

Yes, absolutely. I will let you know once it is ready. I'll keep an eye on the Zulip stream for suggestions.

cesarbm03 commented 1 year ago

Regarding the implementation of the changes, names and the formatting, I found that I can either edit the file on Github or do the changes locally and then force commits to the branch with $ git commit -m "These changes are in response to PR comments" $ git push -f origin HEAD

What's the recommended or best practice for this?

jonweinb commented 1 year ago

Thanks @cesarbm03! Do you have any insights on this @fizruk, @fredrik-bakke?

fizruk commented 1 year ago

Regarding the implementation of the changes, names and the formatting, I found that I can either edit the file on Github or do the changes locally and then force commits to the branch with $ git commit -m "These changes are in response to PR comments" $ git push -f origin HEAD

What's the recommended or best practice for this?

I will note a few things:

  1. Since your PR is not merged yet, it is perfectly fine to push to it.
  2. Editing files on GitHub is okay, but local development is preferrable.
  3. However, I do not think you should "force push", regular push should be enough.
  4. Also, you should push to a specific branch, e.g. formalize-yoneda-embedding-2, not HEAD.
  5. I also see that this PR is not for main, but for formalize-yoneda-embedding branch. Usually, there is no need to do a PR for another PR (and also this PR does not have automated checks because of this) and you can just work on your changes in one branch (and one PR) and we will merge them into main.

I would suggest to merge this PR (it will merge into formalize-yoneda-embedding, not main) and continue working and discussing in #100.

cesarbm03 commented 1 year ago

Thank you for the comments @fizruk and @fredrik-bakke. Once this is merged in #100 I'll make the changes there.

fredrik-bakke commented 1 year ago

Sorry to hold you up!