module Order.Displayed where
Displayed posetsπ
As a special case of displayed categories, we can construct displayed posets: a poset displayed over , written , is a type-theoretic repackaging β so that fibrewise information is easier to recover β of the data of a poset and a monotone map .
record Displayed {ββ βα΅£} β β' (P : Poset ββ βα΅£) : Type (lsuc (β β β') β ββ β βα΅£) where no-eta-equality private module P = Pr P field Ob[_] : P.Ob β Type β Rel[_] : β {x y} β x P.β€ y β Ob[ x ] β Ob[ y ] β Type β' β€-refl' : β {x} {x' : Ob[ x ]} β Rel[ P.β€-refl ] x' x' β€-thin' : β {x y} (f : x P.β€ y) {x' y'} β is-prop (Rel[ f ] x' y') β€-trans' : β {x y z} {x' : Ob[ x ]} {y' : Ob[ y ]} {z' : Ob[ z ]} β {f : x P.β€ y} {g : y P.β€ z} β Rel[ f ] x' y' β Rel[ g ] y' z' β Rel[ P.β€-trans f g ] x' z' β€-antisym' : β {x} {x' y' : Ob[ x ]} β Rel[ P.β€-refl ] x' y' β Rel[ P.β€-refl ] y' x' β x' β‘ y'
β€-antisym-over : β {x y} {f : x P.β€ y} {g : y P.β€ x} {x' y'} β Rel[ f ] x' y' β Rel[ g ] y' x' β PathP (Ξ» i β Ob[ P.β€-antisym f g i ]) x' y' β€-antisym-over {x = x} {f = f} {g} {x'} = transport (Ξ» i β {f : x P.β€ p i} {g : p i P.β€ x} {y' : Ob[ p i ]} β Rel[ f ] x' y' β Rel[ g ] y' x' β PathP (Ξ» j β Ob[ P.β€-antisym f g j ]) x' y') Ξ» r s β transport (Ξ» i β {f g : x P.β€ x} {y' : Ob[ x ]} β Rel[ P.β€-thin P.β€-refl f i ] x' y' β Rel[ P.β€-thin P.β€-refl g i ] y' x' β PathP (Ξ» j β Ob[ P.Ob-is-set _ _ refl (P.β€-antisym f g) i j ]) x' y') β€-antisym' r s where p = P.β€-antisym f g
Analogously to a displayed category, where we can take pairs of an object and an object over to make a new category (the total space ), we can take total spaces of displayed posets to make a new poset.
β« : β {β β' ββ βα΅£} {P : Poset ββ βα΅£} β Displayed β β' P β Poset _ _ β« {P = P} D = po where -- to-poset (Ξ£ β P β D.Ob[_]) mk-β« where module D = Displayed D module P = Pr P po : Poset _ _ po .Poset.Ob = Ξ£ β P β D.Ob[_] po .Poset._β€_ (x , x') (y , y') = Ξ£ (x P.β€ y) Ξ» f β D.Rel[ f ] x' y' po .Poset.β€-thin = Ξ£-is-hlevel 1 P.β€-thin Ξ» f β D.β€-thin' f po .Poset.β€-refl = P.β€-refl , D.β€-refl' po .Poset.β€-trans (p , p') (q , q') = P.β€-trans p q , D.β€-trans' p' q' po .Poset.β€-antisym (p , p') (q , q') = Ξ£-pathp (P.β€-antisym p q) (D.β€-antisym-over p' q') open Displayed
A special case of displayed posets are sub-partial orders, or, (ab)using categorical terminology, full subposets: These are (the total spaces) that result from attaching a proposition to the objects, and leaving the order relation alone.
Full-subposet' : β {ββ βα΅£ β} (P : Poset ββ βα΅£) (S : β P β β Prop β) β Displayed β lzero P Full-subposet' P S .Ob[_] x = β£ S x β£ Full-subposet' P S .Rel[_] f x y = β€ Full-subposet' P S .β€-refl' = tt Full-subposet' P S .β€-thin' f x y = refl Full-subposet' P S .β€-trans' _ _ = tt Full-subposet' P S .β€-antisym' _ _ = is-propβpathp (Ξ» i β S _ .is-tr) _ _ Full-subposet : β {ββ βα΅£ β} (P : Poset ββ βα΅£) (S : β P β β Prop β) β Poset (ββ β β) βα΅£ Full-subposet P S = β« (Full-subposet' P S)