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

Maps of categories, functor categories, and small subprecategories #794

Merged
merged 39 commits into from Sep 26, 2023
Merged

Maps of categories, functor categories, and small subprecategories #794

merged 39 commits into from Sep 26, 2023

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Sep 21, 2023 •
edited

Summary

  • Define the (pre)category of maps of (pre)categories
    • Define maps of (pre)categories
    • Define natural transformations/isomorphisms of maps between (pre)categories
    • Characterize equality of maps between precategories
  • Refactor isomorphisms in small precategories and categories
  • Develop files on natural isomorphisms
  • Define the functor category
    • Characterize equality of functors between precategories
  • Define (small) subprecategories and their precategory structures
  • Define faithful functors (using embeddings, and show that is equivalent to being injective)
  • Define the representing arrow category
  • Composition of large natural transformations

Lots of refactoring in this one.

#769

@fredrik-bakke
Squashed commit of the following:
02f285f 
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 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 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 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
@fredrik-bakke
Copy link
Collaborator Author

I messed up #787, so this one has to take over.

@fredrik-bakke
Copy link
Collaborator Author

So, I've realized that maps of categories should probably form a category by the last extensionality principle I have to formalize. Inside this category, we recover functor categories as full subcategories. Thus natural transformations are useful more generally than for just functors. Moreover, I don't know if perhaps this mapping category is useful when we go to displayed categories. I haven't really looked at any references for that yet, except browsing 1lab a little. In either case, what do you think about defining natural transformations more generally for maps of precategories?

@fredrik-bakke
Copy link
Collaborator Author

Nahh, probably won't need this

@fredrik-bakke fredrik-bakke marked this pull request as ready for review September 24, 2023 15:08
@fredrik-bakke
Copy link
Collaborator Author

Alright, this PR is officially ready for a review now :)

@EgbertRijke
Copy link
Collaborator

If you update this branch, then I'll merge it. I don't have time to look over all of it, but this PR contains many changes that shouldn't be held up too long, and most of it looks good anyway.

fredrik-bakke and others added 8 commits September 26, 2023 07:35
@fredrik-bakke
Merge branch 'master' into functor-categories'
fb04512
@fredrik-bakke @EgbertRijke
Update src/category-theory/category-of-maps-of-categories.lagda.md
950d3df 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/category-of-functors.lagda.md
7c50012 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/category-of-functors.lagda.md
d7819f4 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/adjunctions-large-precategories.lagda.md
b8b890c 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/adjunctions-large-precategories.lagda.md
ab34f6e 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/adjunctions-large-precategories.lagda.md
e447535 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@fredrik-bakke @EgbertRijke
Update src/category-theory/adjunctions-large-precategories.lagda.md
2fdde53 
Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
@EgbertRijke EgbertRijke merged commit e5f5b84 into UniMath:master Sep 26, 2023
4 checks passed
@fredrik-bakke fredrik-bakke deleted the functor-categories' branch September 26, 2023 14:54
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Sep 29, 2023
@fredrik-bakke @EgbertRijke
Maps of categories, functor categories, and small subprecategories (U…
783372e 
…niMath#794)

Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@EgbertRijke EgbertRijke EgbertRijke left review comments

@VojtechStep VojtechStep VojtechStep left review comments

Assignees
No one assigned
Labels
cat-sitting category-theory cleanup foundation refactoring
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@fredrik-bakke @EgbertRijke @VojtechStep