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.has-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 = to-poset (Ξ£ β P β D.Ob[_]) mk-β« where module D = Displayed D module P = Pr P mk-β« : make-poset _ _ mk-β« .make-poset.rel (x , xβ²) (y , yβ²) = Ξ£ (x P.β€ y) Ξ» f β D.Rel[ f ] xβ² yβ² mk-β« .make-poset.id = P.β€-refl , D.β€-reflβ² mk-β« .make-poset.thin = Ξ£-is-hlevel 1 P.β€-thin Ξ» f β D.β€-thinβ² f mk-β« .make-poset.trans (p , pβ²) (q , qβ²) = P.β€-trans p q , D.β€-transβ² pβ² qβ² mk-β« .make-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)