Added isPoset as an analogue for isUnivalent for a Category to Cubical.Relation.Binary.Preorder, copying the CatIso logic with a new record OrderEquiv. ~The naming in this record is quite unfortunate as the upstream library already has a isUnivalent defined for a relation R, saying R is univalent if R a a' is equivalent to a path between a and a'. Suggestions welcome.~
Ripped out our dependency on Cubical.Relation.Binary.Poset completely, and use our definition of a univalent Preorder instead.
Redefined PREORDER and POSET as discussed in #32 .
Got rid of our homebrewed displayed Category and Grothendieck construction, and used the library's instead. Luckily the definitions were basically identical modulo renaming, so this wasn't bad at all. Redefined Posetᴰ as our notion of DisplayedPoset, and fixed the plumbing for the subcategories where morphisms have left adjs, right adjs, and both.
A cool fact -- there were no issues in Hyperdoctrine as our definition of Grothendieck was identical to ∫C!
Fixed the CI pipeline line ending complaint as well.
isPosetas an analogue forisUnivalentfor a Category toCubical.Relation.Binary.Preorder, copying theCatIsologic with a new recordOrderEquiv. ~The naming in this record is quite unfortunate as the upstream library already has aisUnivalentdefined for a relationR, sayingRis univalent ifR a a'is equivalent to a path betweenaanda'. Suggestions welcome.~Cubical.Relation.Binary.Posetcompletely, and use our definition of a univalent Preorder instead.PREORDERandPOSETas discussed in #32 .Posetᴰas our notion ofDisplayedPoset, and fixed the plumbing for the subcategories where morphisms have left adjs, right adjs, and both.Grothendieckwas identical to∫C!