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

Miscellaneous cleanups #1746

Merged
merged 20 commits into from
Sep 3, 2023
Merged

Miscellaneous cleanups #1746

merged 20 commits into from
Sep 3, 2023

Conversation

jdchristensen
Copy link
Collaborator

This PR contains a large number of unrelated cleanups to the library. Each commit is independent, and the library builds after each commit. I recommend reviewing things one commit at a time.

@jdchristensen
Basics/Equivalences: correct the retr and sect names in IsEquivHomotopic
fd4fd62
@jdchristensen
WildCat/Core: add gpd_moveR_M1 (which I didn't end up needing)
2121841
@jdchristensen
Basics/PathGroupoids: concat2_p1/1p are definitionally true
f231d85
@jdchristensen
etc/coqcstriprequires.py: update a comment
57a8724
@jdchristensen
Homotopy/HSpace/Moduli: slightly simplify some proofs
314bca1
@jdchristensen
Pointed/Core: get rid of unneeded lambda expression
b29d56a
@jdchristensen
Fix lots of typos
d48a699
@jdchristensen
PathAny.v: slightly simplify proof of equiv_path_from_contr
828aad4
@jdchristensen
Types/Universe: remove redundant Funext and Univalence hypotheses
18fc1c7
@jdchristensen
Algebra/Groups/Freegroup: simplify and tidy things a bit
7ccd905
@jdchristensen
Basics/Datatypes: remove redundant settings already in Logic.v
e4398ba
@jdchristensen
Types/Unit: get rid of unneeded iota expansion
8cb2be3
@jdchristensen
Basics/Logic: remove duplicate definition of "not"
f5cefb7
@jdchristensen
Basics/PathGroupoids: transport_idmap_ap: make A x y implicit args
e55874f
@jdchristensen
Spaces/Nat: remove redundant proof that n + O = n
9fb36de
@jdchristensen
Basics/Logic: put True and False in Set; adjust comments
37559cb
@jdchristensen
Basics/Overture: remove redundant Arguments commands
5e5da27
@jdchristensen
STYLE.md: give explicit pointer to isequiv_adjointify
bff48d2
Alizter
Alizter approved these changes Sep 2, 2023
View reviewed changes
Copy link
Collaborator

@Alizter Alizter left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM overall. I am unsure about the names in the first commit but it doesn't really matter to me. I trust you are more familiar with the terminology of sections and retractions.

@jdchristensen
Copy link
Collaborator Author

About sect vs retr, you can compare the arguments to Build_IsEquiv to see that the names were reversed before.

jarlg
jarlg reviewed Sep 3, 2023
View reviewed changes
Copy link
Collaborator

@jarlg jarlg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, I only noticed an existing error in WildCat.Core and suggested a correction you can drop in.

About the naming in Spaces.Nat (using a nat_ prefix or not), I agree that leaving a comment is good for future discussion.

theories/WildCat/Core.v Outdated Show resolved Hide resolved
@jdchristensen jdchristensen added this pull request to the merge queue Sep 3, 2023
Merged via the queue into HoTT:master with commit 9481231 Sep 3, 2023
23 checks passed
@jdchristensen jdchristensen deleted the cleanup branch September 3, 2023 14:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jarlg jarlg jarlg left review comments

@Alizter Alizter Alizter approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jdchristensen @jarlg @Alizter