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

Univalent Category of SETOIDs , Setoids are not LCCC #1152

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

Univalent Category of SETOIDs , Setoids are not LCCC #1152

wants to merge 22 commits into from

Commits on Dec 4, 2023

  1. new modules: 

    * Cubical/Categories/Category/Path.agda
  Helper representation of Path between categories to deal with ineficiency in WeakEquivalence.agda
* Cubical/Relation/Binary/Setoid.agda
  Setoid - Pair of hSet and propositional equivalence relation
* Cubical/Categories/Instances/Setoids.agda
  Univalent Category of Setoids

changes:
* Cubical/Categories/Adjoint.agda
  added composiiton of adjunctions
* Cubical/Categories/Equivalence/WeakEquivalence.agda
  Equivalence equivalent to Path for Univalent Categories
* Cubical/Categories/Instances/Functors.agda
  currying of functors is an isomorphism.
* Cubical/Foundations/Transport.agda
  transport-filler-ua = ua-gluePath

+ some other minor helpers
    @marcinjangrzybowski
    marcinjangrzybowski committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    92ccbff View commit details
    Browse the repository at this point in the history

Commits on Dec 5, 2023

  1. simplified transport-filler-ua, as sugested by Tom Jack on Univalent … 

    …Agda Discord
    @marcinjangrzybowski
    marcinjangrzybowski committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    8cd6eeb View commit details
    Browse the repository at this point in the history

  2. formatting fix

    @marcinjangrzybowski
    marcinjangrzybowski committed Dec 5, 2023
    Configuration menu
    Copy the full SHA
    d48cf4b View commit details
    Browse the repository at this point in the history

Commits on Jan 15, 2024

  1. setoids are not LCCC, Sets are

    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 15, 2024
    Configuration menu
    Copy the full SHA
    7ebe15d View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2024

  1. sliced adjoints

    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 21, 2024
    Configuration menu
    Copy the full SHA
    aab1d5e View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2024

  1. wip

    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    b79c431 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/agda/cubical into setoid-… 

    …slice
    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 22, 2024
    Configuration menu
    Copy the full SHA
    f68e19d View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2024

  1. sliced adjoints

    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 28, 2024
    Configuration menu
    Copy the full SHA
    0c5c7cb View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2024

  1. wip

    @marcinjangrzybowski
    marcinjangrzybowski committed Jan 30, 2024
    Configuration menu
    Copy the full SHA
    6d319cb View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2024

  1. Merge remote-tracking branch 'origin2/master' into sliced-adjoints

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    69904be View commit details
    Browse the repository at this point in the history

  2. cleanup

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    c42e230 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'sliced-adjoints' into setoid-slice

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    53650c6 View commit details
    Browse the repository at this point in the history

  4. wip

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    46a83f8 View commit details
    Browse the repository at this point in the history

  5. small fix

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 2, 2024
    Configuration menu
    Copy the full SHA
    03244d0 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2024

  1. cleanup

    @marcinjangrzybowski
    marcinjangrzybowski committed Apr 3, 2024
    Configuration menu
    Copy the full SHA
    b9e9394 View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2024

  1. Merge branch 'master' into sliced-adjoints

    @marcinjangrzybowski
    marcinjangrzybowski authored Sep 2, 2024
    Configuration menu
    Copy the full SHA
    cfeffb0 View commit details
    Browse the repository at this point in the history

  2. small fixes

    @marcinjangrzybowski
    marcinjangrzybowski committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    72cf4ba View commit details
    Browse the repository at this point in the history

  3. removed unviPropEq, replaced its occurence with existing helper

    @marcinjangrzybowski
    marcinjangrzybowski committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    cc3264c View commit details
    Browse the repository at this point in the history

  4. added requested comment

    @marcinjangrzybowski
    marcinjangrzybowski committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    96ca966 View commit details
    Browse the repository at this point in the history

  5. sync

    @marcinjangrzybowski
    marcinjangrzybowski committed Sep 2, 2024
    Configuration menu
    Copy the full SHA
    68c3a44 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. Update Cat.agda 

    removed unifnished code
    @marcinjangrzybowski
    marcinjangrzybowski authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    ac23253 View commit details
    Browse the repository at this point in the history

  2. Update Setoids.agda 

    fixed dead link
    @marcinjangrzybowski
    marcinjangrzybowski authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    d0431e7 View commit details
    Browse the repository at this point in the history