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 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
  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 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 = 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)