open import Cat.Prelude

open import Order.Base

import Order.Reasoning as Pr

module Order.Displayed where


Displayed posetsπ

As a special case of displayed categories, we can construct displayed posets: a poset $P$ displayed over $A$, written $P \mathrel{\htmlClass{liesover}{\hspace{1.366em}}} A$, is a type-theoretic repackaging β so that fibrewise information is easier to recover β of the data of a poset $P$ and a monotone map $P \to A$.

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 $x$ and an object $x'$ over $x$ to make a new category (the total space $\int P$), 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)