-
Notifications
You must be signed in to change notification settings - Fork 71
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
rational commutative monoids #763
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good. I have just one comment.
done |
Ah, now I see why you suggested the opposite naming scheme in my other PR! |
There is the old naming scheme that would give To me it is clear that |
Yep, it definitely makes more sense to me now. I fear the library is wildly inconsistent on this point though. |
I don't want to undertake this refactoring at the moment, or anybody else to do this refactoring... It is more important to finish refactoring the synthetic homotopy theory (which I do intend to work on). |
Yep, very understandable. This is not important at all. Also, I'm not entirely convinced yet. |
This small PR factors out rational commutative monoids from UniMath#623. --------- Co-authored-by: Fredrik Bakke <[email protected]>
commit 6f8fdc1 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 23:22:39 2023 +0200 hom-types are homs commit d7cffc3 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 23:10:50 2023 +0200 `is-set-hom` commit 3a646ce Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 22:53:24 2023 +0200 fix hom-set function categories commit 3bfc7dd Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 22:49:08 2023 +0200 rename hom-sets to `hom-set` commit fd15e21 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 21:42:14 2023 +0200 some comments commit a95c86c Author: Egbert Rijke <[email protected]> Date: Thu Sep 21 12:59:34 2023 +0200 The classification of cyclic rings (UniMath#757) Co-authored-by: izak <[email protected]> commit df1e6e6 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 14:20:56 2023 +0200 consistencies commit 04cf136 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 14:14:52 2023 +0200 add projections initial and terminal objects commit 2ac83c1 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:42:50 2023 +0200 Functors _between_ large... commit 5577dbb Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:33:03 2023 +0200 functors _between_ categories commit 786664f Merge: e0f6858 da7e412 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 12:26:28 2023 +0200 Merge branch 'master' into functor-categories commit e0f6858 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 02:08:26 2023 +0200 pre-commit commit 3933794 Author: Fredrik Bakke <[email protected]> Date: Thu Sep 21 02:06:48 2023 +0200 the functor category and natural isomorphisms commit da7e412 Author: Vojtěch Štěpančík <[email protected]> Date: Wed Sep 20 19:01:16 2023 +0200 Coforks, coequalizers of types, their flattening lemma (UniMath#792) This PR introduces coforks of parallel maps, the dependent and non-dependent universal properties of coequalizers, the construction of coequalizers from pushouts, and the flattening lemma for coequalizers, asserting that sigmas commute with coequalizers. This development mirrors the development of cocones and pushouts. I also changed the statement of the flattening lemma for pushouts to one that sounds more natural to me - we can construct a cocone of sigma types from any cocone, not just a pushout; the previous definition required the vertex to be a pushout in those definitions. Now the statement is "if a cocone is a pushout, then the cocone derived from it is a pushout too". commit d9a8a02 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 03:07:19 2023 +0200 refactor isomorphisms in small (pre-)categories commit f47cf60 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:54:35 2023 +0200 `is-iso` to `is-iso-hom` commit 7955721 Merge: d1a36f7 eda7bb2 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:31:31 2023 +0200 Merge remote-tracking branch 'agda-unimath/master' into functor-categories commit d1a36f7 Author: Fredrik Bakke <[email protected]> Date: Wed Sep 20 00:29:10 2023 +0200 preliminary extensionality of functors commit 30bfd00 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:30:00 2023 +0200 split up definition `functor-precategory-Precategory` commit 3e22d2a Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:14:06 2023 +0200 a little refactoring of natural transformations commit a9f5f27 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 15:13:08 2023 +0200 Use `C` instead of `P` dependent products of precategories commit eda7bb2 Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 22:01:57 2023 +0200 Isomorphisms in large categories and large precategories (UniMath#791) commit cdc008d Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 13:19:50 2023 +0200 Add a dot after the sentence "Content created by..." (UniMath#790) commit a081293 Author: Egbert Rijke <[email protected]> Date: Tue Sep 19 13:01:42 2023 +0200 Add the universal property of identity systems to the overview tables (UniMath#789) commit fec9c63 Merge: 65483f6 9d2c235 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 02:26:31 2023 +0200 Merge branch 'master' into functor-categories commit 65483f6 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 02:25:24 2023 +0200 `comp-natural-transformation-Large-Precategory` and associated refactoring commit 9c166ae Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 00:05:11 2023 +0200 pre-commit commit 08af608 Author: Fredrik Bakke <[email protected]> Date: Tue Sep 19 00:00:34 2023 +0200 prepend `map-` to `(obj/hom)-functor` commit 43ee8e8 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:47:47 2023 +0200 small fixes commit 51ec628 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:21:34 2023 +0200 misc cleanup natural transformations commit 8e6f821 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 23:19:43 2023 +0200 define representing arrow category commit 9d2c235 Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 15:52:57 2023 +0200 Fix website CI (UniMath#786) commit 1bea263 Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 09:52:52 2023 +0200 Always enable git metadata, fetch whole git history in pages CI (UniMath#785) commit b1f027f Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 03:25:35 2023 +0200 Try to fix website CI (UniMath#784) commit 6af959b Author: Vojtěch Štěpančík <[email protected]> Date: Mon Sep 18 03:01:42 2023 +0200 Automatically extract page contributor information during web build (UniMath#770) commit b66c539 Merge: 47f04e3 539174a Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 01:19:20 2023 +0200 Merge branch 'UniMath:master' into functor-categories commit 47f04e3 Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 01:18:42 2023 +0200 links functors between categories commit 539174a Author: Fredrik Bakke <[email protected]> Date: Mon Sep 18 00:39:14 2023 +0200 Yoneda's lemma for categories (UniMath#783) commit 0106784 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 18:05:43 2023 +0200 Moving file about hexagons of identifications (UniMath#782) commit b804ea5 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:45:44 2023 +0200 Update README.md (UniMath#781) commit f7d6658 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:24:59 2023 +0200 Update README.md (UniMath#780) commit f4f4ef2 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:13:37 2023 +0200 Update README.md (UniMath#779) commit 6df85b4 Author: Egbert Rijke <[email protected]> Date: Sun Sep 17 11:08:03 2023 +0200 Fancy title on repo page (UniMath#778) commit 1fb5dc5 Author: maybemabeline <[email protected]> Date: Sat Sep 16 22:32:19 2023 +0200 Equivalence between the first sphere and the circle (UniMath#776) Co-authored-by: Egbert Rijke <[email protected]> commit 1fe0803 Author: Fredrik Bakke <[email protected]> Date: Fri Sep 15 16:18:37 2023 +0200 Define representations of monoids (UniMath#765) commit c813a06 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 15:17:44 2023 +0200 larger image, rounded corners (UniMath#774) commit 0529896 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 13:23:30 2023 +0200 update contributors (UniMath#773) commit 5340335 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 10:58:02 2023 +0200 update contributors, remove unused imports (UniMath#772) commit 533cff1 Author: Egbert Rijke <[email protected]> Date: Fri Sep 15 01:08:32 2023 +0200 Adding an art page (UniMath#771) Co-authored-by: Andrej Bauer <[email protected]> Co-authored-by: Matej Petković <[email protected]> commit adf864e Author: Egbert Rijke <[email protected]> Date: Thu Sep 14 16:44:32 2023 +0200 Symmetric core of a relation (UniMath#754) In this PR we construct the symmetric core of a type valued relation and show that it is the right adjoint of the restriction functor from symmetric relations to relations. Everything we do in this PR is fully coherent and untruncated. --------- Co-authored-by: Fredrik Bakke <[email protected]> commit 50fdf54 Author: Egbert Rijke <[email protected]> Date: Wed Sep 13 19:11:14 2023 +0200 The one-object precategory of a monoid (UniMath#766) commit 413a1bf Author: Vojtěch Štěpančík <[email protected]> Date: Wed Sep 13 18:35:55 2023 +0200 Flattening lemma for pushouts (UniMath#764) commit d826323 Author: Egbert Rijke <[email protected]> Date: Wed Sep 13 17:00:53 2023 +0200 rational commutative monoids (UniMath#763) This small PR factors out rational commutative monoids from UniMath#623. --------- Co-authored-by: Fredrik Bakke <[email protected]>
This small PR factors out rational commutative monoids from #623.