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 be a partial order and be a family of partial orders indexed by the underlying set of We can equip the with a lexicographic partial order:

Note

We avoid the more traditional formulation that uses the strict order:

The reason is that naturally involves when we take the non-strict order as the primitive notion. Negated types carry less information and usually work less well in constructive settings.

Given the dependency of on the comparison between and only makes sense when they lie in the same fibre, that is, when there is evidence We can then transport across to obtain a value in which can then be compared against

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

  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 1
Lexical-sum-over .D.β€-refl' p = F.β€-refl' $sym$ substα΅’-filler-set βFβ (hlevel 2) 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 is essentially 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 2) p _) xβ€y)  We can also define injections from 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 2) 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 and fibres Its mapping-in universal property is: given another poset displayed over and a collection a fibrewise map there exists a (unique!) index-preserving map from the total space of into the lexical sum such that it commutes with  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

Source

The categorical definition of lexicographic sums is given by Reinhard BΓΆrger, Walter Tholen and Anna Tozzi in their paper Lexicographic sums and fibre-faithful maps.