open import Cat.Prelude

open import Data.Id.Base

open import Order.Displayed
open import Order.Morphism
open import Order.Base

import Order.Reasoning as Pr

module Order.Instances.LexicalSum where

Lexicographic sum of posets🔗

private module D = Displayed

module _ {ℓₐ ℓᵣ ℓₐ' ℓᵣ'} (I : Poset ℓₐ ℓᵣ) (F : ⌞ I ⌟ → Poset ℓₐ' ℓᵣ') where
  private
    module I = Pr I
    module F {i : ⌞ I ⌟} = Pr (F i)

    ⌞F⌟ : ⌞ I ⌟ → Type ℓₐ'
    ⌞F⌟ e = ⌞ F e ⌟

Let $I$ be a partial order and $F_{i\in I}$ be a family of partial orders indexed by the underlying set of $I\text{.}$ We can equip the $\Sigma \text{-type}$ ${\Sigma }_{(i:I)}{F}_i$ with a lexicographic partial order:

Given the dependency of $F$ on $I\text{,}$ the comparison between $x:F_i$ and $y:F_j$ only makes sense when they lie in the same fibre, that is, when there is evidence $p:i=j\text{.}$ We can then transport $x$ across $p$ to obtain a value in $F_j\text{,}$ which can then be compared against $y:F_j\text{.}$

The concerns of defining the ordering in each fibre, and then defining the ordering on the entire total space, are mostly orthogonal. Indeed, these can be handled in a modular way: the construction we’re interested in naturally arises as the total (thin) category of a particular displayed order over the base poset $I\text{.}$

  Lexical-sum-over : Displayed _ _ I
  Lexical-sum-over .D.Ob[_]                = ⌞F⌟
  Lexical-sum-over .D.Rel[_] {i} {j} _ x y = (p : i ≡ᵢ j) → substᵢ ⌞F⌟ p x F.≤ y

  Lexical-sum-over .D.≤-thin' _ = hlevel 
  Lexical-sum-over .D.≤-refl' p = F.≤-refl' $ sym $ substᵢ-filler-set ⌞F⌟ (hlevel ) p _
  Lexical-sum-over .D.≤-antisym' x≤'y y≤'x = F.≤-antisym (x≤'y reflᵢ) (y≤'x reflᵢ)
  Lexical-sum-over .D.≤-trans' {f = i≤j} {g = j≤i} x≤'y y≤'z reflᵢ =
    let i=ᵢj = Id≃path.from $ I.≤-antisym i≤j j≤i in
    lemma i=ᵢj (x≤'y i=ᵢj) (y≤'z (symᵢ i=ᵢj))
    where
      lemma : ∀ {i j} (p : i ≡ᵢ j) {x y z} → substᵢ ⌞F⌟ p x F.≤ y → substᵢ ⌞F⌟ (symᵢ p) y F.≤ z → x F.≤ z
      lemma reflᵢ = F.≤-trans

  Lexical-sum : Poset _ _
  Lexical-sum = ∫ Lexical-sum-over

module _ {ℓₐ ℓᵣ ℓₐ' ℓᵣ'} {I : Poset ℓₐ ℓᵣ} {F : ⌞ I ⌟ → Poset ℓₐ' ℓᵣ'} where
  private
    module I = Pr I
    module F {i : ⌞ I ⌟} = Pr (F i)

    ⌞F⌟ : ⌞ I ⌟ → Type ℓₐ'
    ⌞F⌟ e = ⌞ F e ⌟

The fibre in a lexical sum over $i:I$ is essentially $F_i\text{.}$ In fact, their underlying types are judgementally equal in the current construction. We do not express the sameness using isomorphisms in the category of posets (Posets) due to technical reasons: their universe levels do not match and we would need ugly lifting to compensate for the differences.

  lexical-sum-fibre-equiv
    : (i : ⌞ I ⌟) → ⌞ Fibre (Lexical-sum-over I F) i ⌟ ≃ ⌞ F i ⌟
  lexical-sum-fibre-equiv i = _ , id-equiv

  lexical-sum-fibre-equiv-is-order-embedding
    : ∀ i → is-order-embedding (Fibre (Lexical-sum-over I F) i) (F i) (λ x → x)
  lexical-sum-fibre-equiv-is-order-embedding i =
    prop-ext!
      (λ x≤y → x≤y reflᵢ)
      (λ x≤y p → subst (F._≤ _) (substᵢ-filler-set ⌞F⌟ (hlevel ) p _) x≤y)

We can also define injections from $F_i\text{,}$ which are the generic injections fibre-injᵖ (for general displayed posets) precomposed with the inverse of the above equivalence lexical-sum-fibre-equiv.

  lexical-sum-injᵖ : (i : ⌞ I ⌟) → Monotone (F i) (Lexical-sum I F)
  lexical-sum-injᵖ i .hom    x   = i , x
  lexical-sum-injᵖ i .pres-≤ x≤y = I.≤-refl , λ p →
    subst (F._≤ _) (substᵢ-filler-set ⌞F⌟ (hlevel ) p _) x≤y

  lexical-sum-injᵖ-is-order-embedding
    : ∀ i → is-order-embedding (F i) (Lexical-sum I F) (apply (lexical-sum-injᵖ i))
  lexical-sum-injᵖ-is-order-embedding i =
    prop-ext! (lexical-sum-injᵖ i .pres-≤) λ (_ , q) → q reflᵢ

The name Lexical-sum is justified by the observation that it is the maximum poset with the given index $I$ and fibres $F\text{.}$ Its mapping-in universal property is: given another poset $G$ displayed over $I$ and a collection a fibrewise map ${\sigma }_{i\in I}:G_i\to F_i\text{,}$ there exists a (unique!) index-preserving map from the total space of $G$ into the lexical sum such that it commutes with $\sigma \text{.}$

  splitᵖ
    : ∀ {o ℓ} (G : Displayed o ℓ I)
    → (∀ i → Monotone (Fibre G i) (F i))
    → Monotone (∫ G) (Lexical-sum I F)
  splitᵖ G cases .hom    (i , x)     = i , cases i # x
  splitᵖ G cases .pres-≤ (i≤j , x≤y) = i≤j , λ i=ᵢj → lemma-pres-≤ i=ᵢj i≤j x≤y

    where
      module G = D G

      lemma-pres-≤
        : ∀ {i j} (p : i ≡ᵢ j) (i≤j : i I.≤ j) {x y}
        → G.Rel[ i≤j ] x y
        → substᵢ ⌞F⌟ p (cases i .hom x) F.≤ (cases j .hom y)
      lemma-pres-≤ {i = i} reflᵢ i≤j x≤y =
        cases i .pres-≤ $ subst (λ q → G.Rel[ q ] _ _) (I.≤-thin i≤j I.≤-refl) x≤y