open import Cat.Prelude

open import Order.Morphism
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 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

module _ {β„“ β„“' β„“β‚’ β„“α΅£} {P : Poset β„“β‚’ β„“α΅£} (D : Displayed β„“ β„“' P) where
  private
    module D = Displayed D
    module P = Pr P

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.

  ∫ : Poset _ _
  ∫ .Poset.Ob = Σ ⌞ P ⌟ D.Ob[_]
  ∫ .Poset._≀_ (x , x') (y , y') = Ξ£ (x P.≀ y) Ξ» f β†’ D.Rel[ f ] x' y'
  ∫ .Poset.≀-thin = Ξ£-is-hlevel 1 P.≀-thin Ξ» f β†’ D.≀-thin' f
  ∫ .Poset.≀-refl = P.≀-refl , D.≀-refl'
  ∫ .Poset.≀-trans (p , p') (q , q') = P.≀-trans p q , D.≀-trans' p' q'
  ∫ .Poset.≀-antisym (p , p') (q , q') =
    Ξ£-pathp (P.≀-antisym p q) (D.≀-antisym-over p' q')

Similarly, we can define fibre posets as a special case of fibre categories. Because posets are thin categories, we do not worry about most coherence conditions.

  Fibre : ⌞ P ⌟ β†’ Poset _ _
  Fibre x .Poset.Ob = D.Ob[ x ]
  Fibre x .Poset._≀_ = D.Rel[ P.≀-refl ]
  Fibre x .Poset.≀-thin = D.≀-thin' P.≀-refl
  Fibre x .Poset.≀-refl = D.≀-refl'
  Fibre x .Poset.≀-trans p' q' =
    subst (Ξ» p β†’ D.Rel[ p ] _ _) (P.≀-thin _ _) $
    D.≀-trans' p' q'
  Fibre x .Poset.≀-antisym = D.≀-antisym'

There is an injection from any fibre poset to the total space that is an order embedding.

  fibre-injα΅– : (x :  ⌞ P ⌟) β†’ Monotone (Fibre x) ∫
  fibre-injα΅– x .hom    x'    = x , x'
  fibre-injα΅– x .pres-≀ x'≀y' = P.≀-refl , x'≀y'

  fibre-injα΅–-is-order-embedding
    : (x :  ⌞ P ⌟) β†’ is-order-embedding (Fibre x) ∫ (apply (fibre-injα΅– x))
  fibre-injα΅–-is-order-embedding x =
    prop-ext (D.≀-thin' P.≀-refl) (∫ .Poset.≀-thin)
      (fibre-injα΅– x .pres-≀)
      (Ξ» (p , p') β†’ subst (Ξ» p β†’ D.Rel[ p ] _ _) (P.≀-thin p _) p')