Univalent Category of SETOIDs , Setoids are not LCCC

agda / cubical

An experimental library for Cubical Agda

Other

459 stars 141 forks source link

Open marcinjangrzybowski opened 2 months ago

marcinjangrzybowski commented 2 months ago

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 commented 2 months ago

maxsnew commented 2 months ago

A couple of things before a more detailed review:

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"
The link https://people.cs.nott.ac.uk/psznk/docs/setoids.pdf doesn't work for me, I get a 404

marcinjangrzybowski commented 2 months ago

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