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

Conversation

marcinjangrzybowski
Copy link
Contributor

@marcinjangrzybowski marcinjangrzybowski commented Sep 2, 2024 •
edited
Loading

Cubical/Relation/Binary/Setoid.agda

  • Setoid as Pair of hSet and propositional equivalence relation

Cubical/Categories/Instances/Setoids.agda

  • Univalent Category of Setoids
  • Adjoint quadruple of functors from/to SET : Quot ⊣ IdRel ⊣ Forget ⊣ FullRel (crude, basic cohesion?)
  • ¬BaseChange⊣SetoidΠ - Base change functor does not have right adjoint (so SETOID cannot be LCCC, at least not in the literal sense) implementation of Setoids are not an LCCC by Thorsten Altenkirch and Nicolai Kraus (https://nicolaikraus.github.io/docs/setoids.pdf)

@marcinjangrzybowski
new modules:
92ccbff 
* 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
simplified transport-filler-ua, as sugested by Tom Jack on Univalent …
8cd6eeb 
…Agda Discord
@marcinjangrzybowski
formatting fix
d48cf4b
@marcinjangrzybowski
setoids are not LCCC, Sets are
7ebe15d
@marcinjangrzybowski
sliced adjoints
aab1d5e
@marcinjangrzybowski
wip
b79c431
@marcinjangrzybowski
Merge branch 'master' of https://github.com/agda/cubical into setoid-…
f68e19d 
…slice
@marcinjangrzybowski
sliced adjoints
0c5c7cb
@marcinjangrzybowski
wip
6d319cb
@marcinjangrzybowski
Merge remote-tracking branch 'origin2/master' into sliced-adjoints
69904be
@marcinjangrzybowski
cleanup
c42e230
@marcinjangrzybowski
Merge branch 'sliced-adjoints' into setoid-slice
53650c6
@marcinjangrzybowski
wip
46a83f8
@marcinjangrzybowski
small fix
03244d0
@marcinjangrzybowski
cleanup
b9e9394
@marcinjangrzybowski
Merge branch 'master' into sliced-adjoints
cfeffb0
@marcinjangrzybowski
small fixes
72cf4ba
@marcinjangrzybowski
removed unviPropEq, replaced its occurence with existing helper
cc3264c
@marcinjangrzybowski
added requested comment
96ca966
@marcinjangrzybowski
sync
68c3a44
@marcinjangrzybowski
Copy link
Contributor Author

Depends on #1120

@marcinjangrzybowski marcinjangrzybowski marked this pull request as draft September 2, 2024 23:35
@marcinjangrzybowski
Update Cat.agda
ac23253 
removed unifnished code
@maxsnew maxsnew self-assigned this Sep 10, 2024
@maxsnew
Copy link
Collaborator

maxsnew commented Sep 10, 2024

A couple of things before a more detailed review:

  1. I don't think we should commit to the terminology "Setoid" for this, as often a Setoid is defined as coming with a Type-valued relation rather than a Prop-valued relation. I would suggest we just call these "equivalence relations" or even "thin groupoid"
  2. The link https://people.cs.nott.ac.uk/psznk/docs/setoids.pdf doesn't work for me, I get a 404

@marcinjangrzybowski
Copy link
Contributor Author

  1. Updated the link to working one: https://nicolaikraus.github.io/docs/setoids.pdf
    2.I will change terminology.

@marcinjangrzybowski
Update Setoids.agda
d0431e7 
fixed dead link
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@maxsnew maxsnew

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@marcinjangrzybowski @maxsnew