-
Notifications
You must be signed in to change notification settings - Fork 5
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.
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
Preorder Refactor #41
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Need a few fixes
variable | ||
ℓC ℓC' ℓCᴰ ℓCᴰ' : Level | ||
|
||
record Posetᴰ (C : Category ℓC ℓC') ℓCᴰ ℓCᴰ' : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be Preorderᴰ
since it doesn't require univalence/anti-symmetry
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also should probably document somewhere that these are equivalent to categories with a faithful functor into C.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Added the functor and the faithful proof from Grothendieck.agda to Displayed/Preorder.agda.
module _ {C : Category ℓC ℓC'} where | ||
open Functor | ||
|
||
Fst : {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} → Functor (∫C Cᴰ) C |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should go in Displayed.Base
upstream but for now put it in Displayed.Base.More
so we know to do that when we PR. It certainly doesn't belong in Displayed.Preorder
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done.
e7bc6dd
to
dbacb50
Compare
isPoset
as an analogue forisUnivalent
for a Category toCubical.Relation.Binary.Preorder
, copying theCatIso
logic with a new recordOrderEquiv
.The naming in this record is quite unfortunate as the upstream library already has aisUnivalent
defined for a relationR
, sayingR
is univalent ifR a a'
is equivalent to a path betweena
anda'
. Suggestions welcome.Cubical.Relation.Binary.Poset
completely, and use our definition of a univalent Preorder instead.PREORDER
andPOSET
as discussed in Modular Formulation of Preorders, Posets, HeytAlg, etc #32 .Posetᴰ
as our notion ofDisplayedPoset
, and fixed the plumbing for the subcategories where morphisms have left adjs, right adjs, and both.Grothendieck
was identical to∫C
!