Concrete groups #254
Merged
Concrete groups #254
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ncfavier
force-pushed
the
concrete-groups
branch
from
3726cfc
to
5416169
Compare
ncfavier
force-pushed
the
concrete-groups
branch
from
5416169
to
c1b97c6
Compare
Using find and xargs runs into problems when using Nix, because stack creates a command line that exceeds xargs' margin and therefore ARG_MAX.
Also fix context extension in `decompose-is-hlevel-top` so that we can descend under more than one binder.
plt-amy
requested changes
Sep 4, 2023
plt-amy
approved these changes
Sep 4, 2023
|
Thanks! |
ncfavier
commented
Dec 26, 2023
Comment on lines
+193
to
+203
| π₁B : ConcreteGroup ℓ → Group ℓ | ||
| π₁B G = to-group mk where | ||
| open make-group | ||
| mk : make-group (pt G ≡ pt G) | ||
| mk .group-is-set = G .has-is-groupoid _ _ | ||
| mk .unit = refl | ||
| mk .mul = _∙_ | ||
| mk .inv = sym | ||
| mk .assoc = ∙-assoc | ||
| mk .invl = ∙-inv-l | ||
| mk .idl = ∙-id-l |
There was a problem hiding this comment.
Oh, we already had π₁Groupoid 🤦
There was a problem hiding this comment.
Oh yeah. I'll unify the two in my next PR
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Defines connectedness, concrete groups (pointed connected groupoids), and an equivalence between the categories of concrete and abstract (set-based) groups.
The section on delooping homomorphisms is largely inspired by [Symmetry §4.10], which was apparently written by Thierry Coquand(?).
I'm not sure how to best organise concepts into modules in a way that avoids cyclic dependencies. If you have any ideas at all, please advise. Currently things are kind of strewn about between
1Lab.Type.Pointed,1Lab.Connectedness,Algebra.Group.Homotopy,Homotopy.Base, and nowAlgebra.Group.Concrete, with all sorts of 🐔🔄🥚 problems lurking around the corner.Rendered
Checklist
Before submitting a merge request, please check the items below:
The imports are sorted (use
find -type f -name \*.agda -or -name \*.lagda.md | xargs support/sort-imports.hs)All code blocks have "agda" as their language. This is so that
tools like Tokei can report accurate line counts for proofs vs. text.
Proofs are explained to a satisfactory degree; This is subjective,
of course, but proofs should be comprehensible to a hypothetical human
whose knowledge is limited to a working understanding of non-cubical
Agda, and the stuff your pages link to.
The following items are encouraged, but optional:
If you feel comfortable, add yourself to the Authors page! Add a
profile picture that's recognisably "you" under support/pfps; The
picture should be recognisable at 128x128px, should look good in a
squircle, and shouldn't be more than 200KiB.
If your contribution makes mention of a negative statement, but
does not prove the negative (perhaps because it would distract from the
main point), consider adding it to the counterexamples folder.
If a proof can be done in both "cubical style", and "book HoTT
style", and you have the energy to do both, consider doing both!
However, it is completely fine to only do one! For instance, I
(Amélia) am much better at writing proofs "book-style".
If a commit affects many files without adding any content and you don't
want your name to appear on those pages (for example, treewide refactorings
or reformattings), start the commit message with
chore:or include the wordNOAUTHORanywhere.