Good names for Prop-based relations?

[JacquesCarette]

I'm experimenting with rebuilding a Category library with _≡_ based on Prop instead of Set. So I need to rebuild most of Relation.Binary (and likely more) to be in Prop.

So Relation.Binary.Prop ? Relation.Prop.Binary? The latter is likely more extensible for when inevitably Unary and so on are needed too. And there'll be Setoid reasoning and ... too.

[JacquesCarette]

Well, that certainly won't work, as Prop is a keyword, and that module name doesn't even parse. Relation.Propositional.Binary ? Relation.Classical.Binary ? Relation.Squashed.Binary ?

[MatthewDaggitt]

Hmm it's unpleasant that it all needs to be duplicated. What we really need is some method of being polymorphic over both Set and Prop. Calling @jespercockx for ideas!

In the short term, I think the word (whatever we choose to call it) should be promoted even higher (e.g. Propositional.Relation.Binary). I probably prefer Propositional over Classical or Squashed...

[JacquesCarette]

Ok, I can do that. Moving it (before it's been merged) is not a big deal.

[gallais]

I would expect Proposition.Binary rather than Propositional.Relation.Binary.
But rather than duplicating everything, is it not possible to embed a Prop into a
Set and use that as your notion of equivalence? This way you can reuse the old
structures but still enjoy the stronger equality.

Cf. #645 for a bare bones example.

[jespercockx]

See agda/agda#3328 for the issue of defining functions polymorphically over Prop and Set. @andreasabel has a proposal there to make Prop/Set into another dimension (like levels) instead of a fully separate thing like it is now. Another idea (which would subsume this one) is to expose a new type Sort and allow the user to define her own sorts and sort families to be polymorpic over.

[HuStmpHrrr]

oh really?? you do need to rebuild every for Prop? what's the worst part of Coq and I really don't want to see that happening in Agda.

Aside, is there any particular reason to make relations in Prop instead of Set?

[JacquesCarette]

As far as I can tell, the Categories library relies quite heavily on proof irrelevance, especially for higher operations. Things like horizontal and vertical composition of natural transformations wouldn't go through at all without it, because certain things are supposed to be definitionally equal -- and they are, if you ignore the proofs. There are other parts too that go weird in the proof-relevant setting, but I forget.

I am not wedded to using Prop. All I want is a stable Categories library - I'll entertain any design that allows that and is still recognizable as "category theory". Personally, I would be very happy to be able to develop proof-relevant category theory; but I don't want to do it at the cost of using transport and heterogeneous equality all over the place. That can be someone else's cubical-agda project.

[jespercockx]

oh really?? you do need to rebuild every for Prop? what's the worst part of Coq and I really don't want to see that happening in Agda.
--

At the moment, yes. PRs welcome.

[JacquesCarette]

Note this particular issue is moot, in the sense that we've decided to do "proof-relevant category theory" instead. And it is currently working just fine.

There were some issues brought about because this basically means doing work with bicategories (i.e. weak 2-categories), but all fixeable up to now. [Details documented in the issues over in the agda-categories repo.]