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

rational commutative monoids #763

Merged
merged 4 commits into from
Sep 13, 2023

Conversation

EgbertRijke
Copy link
Collaborator

This small PR factors out rational commutative monoids from #623.

Copy link
Collaborator

@fredrik-bakke fredrik-bakke left a 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.

src/group-theory/rational-commutative-monoids.lagda.md Outdated Show resolved Hide resolved
@EgbertRijke
Copy link
Collaborator Author

done

@fredrik-bakke
Copy link
Collaborator

Ah, now I see why you suggested the opposite naming scheme in my other PR!

@EgbertRijke
Copy link
Collaborator Author

There is the old naming scheme that would give is-rational-Commutative-Monoid-Prop, but I started to really dislike this because we only do something odd like this for propositions, and it goes against the rest of the naming scheme. So I thought, ok we start with an object, construct a proposition, and that proposition has a name, so the naming scheme should be [name]-prop-[Namespace] where Namespace is the name of a category that we kind of treat like an artificial namespace. For example Ring, Group, or Commutative-Monoid.

To me it is clear that [name]-prop-Commutative-Monoid would take a context with a commutative monoid featuring prominently in it, and construct a proposition. That proposition then has name [name]. Idk... to me it makes sense and it fits well with the rest of the naming scheme.

@fredrik-bakke
Copy link
Collaborator

Yep, it definitely makes more sense to me now. I fear the library is wildly inconsistent on this point though.

@EgbertRijke
Copy link
Collaborator Author

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).

@fredrik-bakke
Copy link
Collaborator

Yep, very understandable. This is not important at all. Also, I'm not entirely convinced yet.

@fredrik-bakke fredrik-bakke merged commit d826323 into UniMath:master Sep 13, 2023
4 checks passed
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
This small PR factors out rational commutative monoids from UniMath#623.

---------

Co-authored-by: Fredrik Bakke <[email protected]>
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants