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

Isomorphisms in large categories and large precategories #791

Merged
merged 2 commits into from
Sep 19, 2023
Merged

Isomorphisms in large categories and large precategories #791

merged 2 commits into from
Sep 19, 2023

Conversation

EgbertRijke
Copy link
Collaborator

This PR adds a file for isomoprhisms in large categories. Furthermore, it cleans up and refactors the file about isomorphisms in large precategories, and it also adds the theorems that a morphism is an isomorphism if and only if pre/postcomposition is an equivalence.

@EgbertRijke EgbertRijke merged commit eda7bb2 into UniMath:master Sep 19, 2023
4 checks passed
@EgbertRijke EgbertRijke deleted the isomorphisms branch September 19, 2023 20:01
fredrik-bakke
fredrik-bakke reviewed Sep 19, 2023
View reviewed changes
src/category-theory/large-precategories.lagda.md
Comment on lines +123 to +141
precomp-hom-Large-Precategory :
{l1 l2 l3 : Level}
{X : obj-Large-Precategory C l1}
{Y : obj-Large-Precategory C l2}
(f : type-hom-Large-Precategory X Y) →
(Z : obj-Large-Precategory C l3) →
type-hom-Large-Precategory Y Z → type-hom-Large-Precategory X Z
precomp-hom-Large-Precategory f Z g =
comp-hom-Large-Precategory C g f

postcomp-hom-Large-Precategory :
{l1 l2 l3 : Level}
(X : obj-Large-Precategory C l1)
{Y : obj-Large-Precategory C l2}
{Z : obj-Large-Precategory C l3}
(f : type-hom-Large-Precategory Y Z) →
type-hom-Large-Precategory X Y → type-hom-Large-Precategory X Z
postcomp-hom-Large-Precategory X f g =
comp-hom-Large-Precategory C f g
Copy link
Collaborator

Choose a reason for hiding this comment

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

I put these under their own sections for small (pre)categories

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Ah, ok, perhaps you can sneak that into your categories PR:)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks for taking a look!

@fredrik-bakke
Copy link
Collaborator

Damn, too slow 😞

@EgbertRijke
Copy link
Collaborator Author

Sorry!

fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 21, 2023
@EgbertRijke @fredrik-bakke
Isomorphisms in large categories and large precategories (UniMath#791)
e7994e4
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 <fredrbak@gmail.com>
Date:   Thu Sep 21 23:22:39 2023 +0200

    hom-types are homs

commit d7cffc3
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 23:10:50 2023 +0200

    `is-set-hom`

commit 3a646ce
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 22:53:24 2023 +0200

    fix hom-set function categories

commit 3bfc7dd
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 22:49:08 2023 +0200

    rename hom-sets to `hom-set`

commit fd15e21
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 21:42:14 2023 +0200

    some comments

commit a95c86c
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Thu Sep 21 12:59:34 2023 +0200

    The classification of cyclic rings (UniMath#757)

    Co-authored-by: izak <gregapercic000@gmail.com>

commit df1e6e6
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 14:20:56 2023 +0200

    consistencies

commit 04cf136
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 14:14:52 2023 +0200

    add projections initial and terminal objects

commit 2ac83c1
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:42:50 2023 +0200

    Functors _between_ large...

commit 5577dbb
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:33:03 2023 +0200

    functors _between_ categories

commit 786664f
Merge: e0f6858 da7e412
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 12:26:28 2023 +0200

    Merge branch 'master' into functor-categories

commit e0f6858
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 02:08:26 2023 +0200

    pre-commit

commit 3933794
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Thu Sep 21 02:06:48 2023 +0200

    the functor category and natural isomorphisms

commit da7e412
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
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 <fredrbak@gmail.com>
Date:   Wed Sep 20 03:07:19 2023 +0200

    refactor isomorphisms in small (pre-)categories

commit f47cf60
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:54:35 2023 +0200

    `is-iso` to `is-iso-hom`

commit 7955721
Merge: d1a36f7 eda7bb2
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:31:31 2023 +0200

    Merge remote-tracking branch 'agda-unimath/master' into functor-categories

commit d1a36f7
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Wed Sep 20 00:29:10 2023 +0200

    preliminary extensionality of functors

commit 30bfd00
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:30:00 2023 +0200

    split up definition `functor-precategory-Precategory`

commit 3e22d2a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:14:06 2023 +0200

    a little refactoring of natural transformations

commit a9f5f27
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 15:13:08 2023 +0200

    Use `C` instead of `P` dependent products of precategories

commit eda7bb2
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Tue Sep 19 22:01:57 2023 +0200

    Isomorphisms in large categories and large precategories (UniMath#791)

commit cdc008d
Author: Egbert Rijke <e.m.rijke@gmail.com>
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 <e.m.rijke@gmail.com>
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 <fredrbak@gmail.com>
Date:   Tue Sep 19 02:26:31 2023 +0200

    Merge branch 'master' into functor-categories

commit 65483f6
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 02:25:24 2023 +0200

    `comp-natural-transformation-Large-Precategory` and associated refactoring

commit 9c166ae
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 00:05:11 2023 +0200

    pre-commit

commit 08af608
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Tue Sep 19 00:00:34 2023 +0200

    prepend `map-` to `(obj/hom)-functor`

commit 43ee8e8
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:47:47 2023 +0200

    small fixes

commit 51ec628
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:21:34 2023 +0200

    misc cleanup natural transformations

commit 8e6f821
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 23:19:43 2023 +0200

    define representing arrow category

commit 9d2c235
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 15:52:57 2023 +0200

    Fix website CI (UniMath#786)

commit 1bea263
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
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 <vojtechstepancik@outlook.com>
Date:   Mon Sep 18 03:25:35 2023 +0200

    Try to fix website CI (UniMath#784)

commit 6af959b
Author: Vojtěch Štěpančík <vojtechstepancik@outlook.com>
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 <fredrbak@gmail.com>
Date:   Mon Sep 18 01:19:20 2023 +0200

    Merge branch 'UniMath:master' into functor-categories

commit 47f04e3
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 01:18:42 2023 +0200

    links functors between categories

commit 539174a
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Mon Sep 18 00:39:14 2023 +0200

    Yoneda's lemma for categories (UniMath#783)

commit 0106784
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 18:05:43 2023 +0200

    Moving file about hexagons of identifications (UniMath#782)

commit b804ea5
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:45:44 2023 +0200

    Update README.md (UniMath#781)

commit f7d6658
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:24:59 2023 +0200

    Update README.md (UniMath#780)

commit f4f4ef2
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:13:37 2023 +0200

    Update README.md (UniMath#779)

commit 6df85b4
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Sun Sep 17 11:08:03 2023 +0200

    Fancy title on repo page (UniMath#778)

commit 1fb5dc5
Author: maybemabeline <142519092+maybemabeline@users.noreply.github.com>
Date:   Sat Sep 16 22:32:19 2023 +0200

    Equivalence between the first sphere and the circle (UniMath#776)

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>

commit 1fe0803
Author: Fredrik Bakke <fredrbak@gmail.com>
Date:   Fri Sep 15 16:18:37 2023 +0200

    Define representations of monoids (UniMath#765)

commit c813a06
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 15:17:44 2023 +0200

    larger image, rounded corners (UniMath#774)

commit 0529896
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 13:23:30 2023 +0200

    update contributors (UniMath#773)

commit 5340335
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 10:58:02 2023 +0200

    update contributors, remove unused imports (UniMath#772)

commit 533cff1
Author: Egbert Rijke <e.m.rijke@gmail.com>
Date:   Fri Sep 15 01:08:32 2023 +0200

    Adding an art page (UniMath#771)

    Co-authored-by: Andrej Bauer <andrej.bauer@andrej.com>
    Co-authored-by: Matej Petković <Petkomat@users.noreply.github.com>

commit adf864e
Author: Egbert Rijke <e.m.rijke@gmail.com>
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 <fredrbak@gmail.com>

commit 50fdf54
Author: Egbert Rijke <e.m.rijke@gmail.com>
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 <vojtechstepancik@outlook.com>
Date:   Wed Sep 13 18:35:55 2023 +0200

    Flattening lemma for pushouts (UniMath#764)

commit d826323
Author: Egbert Rijke <e.m.rijke@gmail.com>
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 <fredrbak@gmail.com>
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
Projects
None yet
Milestone
No milestone
Development

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