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

Beyond finite sets #623

Draft
wants to merge 33 commits into
base: master
Choose a base branch
from
Draft

Beyond finite sets #623

wants to merge 33 commits into from

Conversation

EgbertRijke
Copy link
Collaborator

@EgbertRijke EgbertRijke commented May 15, 2023 •
edited

This PR adds the following files to the library:

  • Foundation
    • Symmetric cores of binary relations
  • Graph Theory
    • The forgetful functor from directed graphs to undirected graphs
    • The forgetful functor from undirected graphs to directed graphs
    • The undirected core of a directed graph
    • Walks in finite undirected graphs
  • Group Theory
    • Powers of elements in commutative monoids
    • Rational commutative monoids
  • Trees
    • Finite undirected trees
  • Univalent combinatorics
    • The category of cyclically ordered sets
    • Morphisms of cyclic types
    • Omega-finite types
    • The reduced 1-bordism category
    • Symmetric operations
    • Unordered pairs of elements of finite types

The topic formalized in this PR were topics of discussion during the Beyond Finite Sets meeting. Results expected to be formalized in this PR are:

  • Show that the type of undirected trees with n nodes is pi-finite, and obtain the function that returns for each n the number of unlabeled trees with n nodes
  • Equip the 1-bordism category with the structure of a category.

@EgbertRijke EgbertRijke mentioned this pull request Sep 11, 2023
Merged
@EgbertRijke EgbertRijke mentioned this pull request Sep 11, 2023
Merged
fredrik-bakke pushed a commit that referenced this pull request Sep 12, 2023
@EgbertRijke
Beyond foundation (#751)
58eb0fc 
In this PR I pulled changes I made in the `foundation` and
`foundation-core` folders in the Beyond finite sets PR #623. The goal is
to create something mergeable without having to wait for the other
unfinished changes in #623. Let's see what monstrosity I created.
@EgbertRijke EgbertRijke mentioned this pull request Sep 13, 2023
Merged
fredrik-bakke added a commit that referenced this pull request Sep 13, 2023
@EgbertRijke @fredrik-bakke
rational commutative monoids (#763)
d826323 
This small PR factors out rational commutative monoids from #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
@EgbertRijke @fredrik-bakke
rational commutative monoids (UniMath#763)
20c7370 
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
@fredrik-bakke
Squashed commit of the following:
a6b6523 
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]>
fredrik-bakke
fredrik-bakke reviewed Jan 2, 2024
View reviewed changes
src/univalent-combinatorics/omega-finite-types.lagda.md
Copy link
Collaborator

Choose a reason for hiding this comment

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

Could "ω-Finite types" as you define them here also faithfully be called "profinite types"?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

You can only call something a pro-object if it is an object of the procompletion of your category, in this case types. Pro types should have many nice properties which omega-finite types don’t have, such as being closed under retracts.

In general in Agda-unimath, we shouldn’t try to be too fancy with terminology. When we define a concept, it should be obvious that it is defined in the expected way.

Copy link
Collaborator

Choose a reason for hiding this comment

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

You mean the procompletion of finite types and maps of finite types, right?

Copy link
Collaborator

Choose a reason for hiding this comment

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

My comment was not meant as a suggestion, but merely as a question arising from curiosity.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fredrik-bakke fredrik-bakke fredrik-bakke left review comments

Assignees
No one assigned
Labels
category-theory cleanup graph-theory group-theory refactoring trees univalent-combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@EgbertRijke @fredrik-bakke