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

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

Merged
merged 39 commits into from Sep 26, 2023

Commits on Sep 21, 2023

  1. Squashed commit of the following:

    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 committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    02f285f View commit details
    Browse the repository at this point in the history
  2. revert map- functor

    fredrik-bakke committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    ac7a324 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2023

  1. Configuration menu
    Copy the full SHA
    268fa3e View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    8775005 View commit details
    Browse the repository at this point in the history
  3. maps of categories

    fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    b542db6 View commit details
    Browse the repository at this point in the history
  4. resolve dependencies

    fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    5307f45 View commit details
    Browse the repository at this point in the history
  5. remove unused imports

    fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    37785b6 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    323553e View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    c6884ac View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    ea83555 View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    519a530 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    8fd2f66 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    f787045 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    28ae519 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    bda6d3a View commit details
    Browse the repository at this point in the history
  14. large subcategories

    EgbertRijke authored and fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    041ac96 View commit details
    Browse the repository at this point in the history
  15. Configuration menu
    Copy the full SHA
    7882d75 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    e87ae6d View commit details
    Browse the repository at this point in the history
  17. The inclusion functor

    fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    7e0954e View commit details
    Browse the repository at this point in the history
  18. Configuration menu
    Copy the full SHA
    ffb8bdf View commit details
    Browse the repository at this point in the history
  19. faithful functors

    fredrik-bakke committed Sep 23, 2023
    Configuration menu
    Copy the full SHA
    4f91088 View commit details
    Browse the repository at this point in the history
  20. Configuration menu
    Copy the full SHA
    80c1f53 View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2023

  1. Configuration menu
    Copy the full SHA
    6db98b8 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    240c242 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    4c6193d View commit details
    Browse the repository at this point in the history
  4. lingering comments

    fredrik-bakke committed Sep 24, 2023
    Configuration menu
    Copy the full SHA
    4b2a93d View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    c2c737c View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    aa16562 View commit details
    Browse the repository at this point in the history
  7. self-review part 2

    fredrik-bakke committed Sep 24, 2023
    Configuration menu
    Copy the full SHA
    a5603e1 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    4d8d60c View commit details
    Browse the repository at this point in the history
  9. fix links

    fredrik-bakke committed Sep 24, 2023
    Configuration menu
    Copy the full SHA
    344deb1 View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2023

  1. Configuration menu
    Copy the full SHA
    fb04512 View commit details
    Browse the repository at this point in the history
  2. Update src/category-theory/category-of-maps-of-categories.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    950d3df View commit details
    Browse the repository at this point in the history
  3. Update src/category-theory/category-of-functors.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    7c50012 View commit details
    Browse the repository at this point in the history
  4. Update src/category-theory/category-of-functors.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    d7819f4 View commit details
    Browse the repository at this point in the history
  5. Update src/category-theory/adjunctions-large-precategories.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    b8b890c View commit details
    Browse the repository at this point in the history
  6. Update src/category-theory/adjunctions-large-precategories.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    ab34f6e View commit details
    Browse the repository at this point in the history
  7. Update src/category-theory/adjunctions-large-precategories.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    e447535 View commit details
    Browse the repository at this point in the history
  8. Update src/category-theory/adjunctions-large-precategories.lagda.md

    Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
    fredrik-bakke and EgbertRijke committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    2fdde53 View commit details
    Browse the repository at this point in the history