module Order.Displayed where

Displayed posetsπŸ”—

As a special case of displayed categories, we can construct displayed posets: a poset PP displayed over AA, written PAP \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 PP and a monotone map P→AP \to A.

record Displayed {β„“β‚’ β„“α΅£} β„“ β„“' (P : Poset β„“β‚’ β„“α΅£) : Type (lsuc (β„“ βŠ” β„“') βŠ” β„“β‚’ βŠ” β„“α΅£) where

  private module P = Pr P

    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')
      : βˆ€ {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'
      : βˆ€ {x} {x' y' : Ob[ x ]}
      β†’ Rel[ P.≀-refl ] x' y' β†’ Rel[ P.≀-refl ] y' x' β†’ x' ≑ y'

Analogously to a displayed category, where we can take pairs of an object xx and an object xβ€²x' over xx to make a new category (the total space ∫P\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.

  : βˆ€ {β„“β‚’ β„“α΅£ β„“} (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) _ _

  : βˆ€ {β„“β‚’ β„“α΅£ β„“} (P : Poset β„“β‚’ β„“α΅£) (S : ⌞ P ⌟ β†’ Prop β„“)
  β†’ Poset (β„“β‚’ βŠ” β„“) β„“α΅£
Full-subposet P S = ∫ (Full-subposet' P S)