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

Symmetric core of a relation #754

Merged
merged 21 commits into from
Sep 14, 2023
Merged

Symmetric core of a relation #754

merged 21 commits into from
Sep 14, 2023

Conversation

EgbertRijke
Copy link
Collaborator

@EgbertRijke EgbertRijke commented Sep 11, 2023 •
edited
Loading

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.

@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
22800e1 
…ic-core
@EgbertRijke
adding further explanation
8e754a4
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
480a1c6 
…ic-core
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
deb57b2 
…ic-core
@EgbertRijke
make library compile
1db6370
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
49b63ba 
…ic-core
@EgbertRijke
work
8fbfb54
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
1149bb8 
…ic-core
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
8b3645c 
…ic-core
@EgbertRijke
work
9597126
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into symmetr…
a8a6ee2 
…ic-core
@EgbertRijke
work on 2-element types
ce3b700
@EgbertRijke
refactor 2-element types
745daca
@EgbertRijke
the restriction-core adjunction of relations and symmetric relations
5118e77
@EgbertRijke EgbertRijke marked this pull request as ready for review September 13, 2023 23:52
@EgbertRijke
Copy link
Collaborator Author

Ready for review

@fredrik-bakke
Copy link
Collaborator

I also noticed there are some counterexamples in the file about 2-element types. I think that's quite nice, and actually wish there were more of them in the library. Although sometimes less "useful", they go a long way by showing what sort of limitations concepts have, and give a sense of how one should think about them and what the authors of the files care about.

@EgbertRijke
Copy link
Collaborator Author

I also noticed there are some counterexamples in the file about 2-element types. I think that's quite nice, and actually wish there were more of them in the library. Although sometimes less "useful", they go a long way by showing what sort of limitations concepts have, and give a sense of how one should think about them and what the authors of the files care about.

I agree 100%. Examples and counterexamples are an essential part of mathematics and they should be included in the library. General theories are easy to formalize, but good examples are actually often quite hard. For example, it would be quite nice if someone could characterize the Zariski spectrum of the integers, but I would expect this formalization to be quite elaborate and perhaps messy.

@EgbertRijke
Copy link
Collaborator Author

Thank you for the feedback! I addressed all comments.

@fredrik-bakke
Copy link
Collaborator

hmm, looks like you have to run pre-commit again

@EgbertRijke
Copy link
Collaborator Author

Strange. I did that. But I'll do it again.

@EgbertRijke
Copy link
Collaborator Author

The issue was that I carried an untracked file from one branch to another:)

@fredrik-bakke fredrik-bakke merged commit adf864e into UniMath:master Sep 14, 2023
4 checks passed
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
@EgbertRijke @fredrik-bakke
Symmetric core of a relation (UniMath#754)
15a4996 
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]>
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]>
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 approved these changes

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

Successfully merging this pull request may close these issues.
2 participants
@EgbertRijke @fredrik-bakke