open import Cat.Diagram.Coproduct.Indexed
open import Cat.Morphism
open import Cat.Prelude

open import Data.Id.Base
open import Data.Bool
open import Data.Sum

open import Order.Instances.Coproduct renaming (matchα΅– to matchβŠŽα΅–)
open import Order.Instances.Discrete
open import Order.Displayed
open import Order.Univalent
open import Order.Morphism
open import Order.Base

import Order.Reasoning as Pr

open is-indexed-coproduct
open Indexed-coproduct
open Inverses

module Order.Instances.Disjoint where

Indexed coproducts of posetsπŸ”—

If is a family of partial orders indexed by a set then we can equip the with a β€œfibrewise” partial order: this is the coproduct of these orders in the category of posets.

private module D = Displayed

module _ {β„“ ℓₐ β„“α΅£} (I : Set β„“) (F : ⌞ I ⌟ β†’ Poset ℓₐ β„“α΅£) where
  private
    open module F {i : ⌞ I ⌟} = Pr (F i)

    ⌞F⌟ : ⌞ I ⌟ β†’ Type ℓₐ
    ⌞F⌟ e = ⌞ F e ⌟

Since the indices are drawn from completely arbitrary sets, we can’t exactly define the order by pattern matching, as in the binary coproduct of posets. Instead, we must define what it means to compare two totally arbitrary pairs 1.

Considering that we only know how to compare elements in the same fibre, the natural solution is to require, as part of proving some evidence We can then transport across to obtain a value in which can 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 discrete partial order on the index set 

  _≀[_]'_ : {i j : ⌞ I ⌟} β†’ ⌞F⌟ i β†’ i ≑ᡒ j β†’ ⌞F⌟ j β†’ Type β„“α΅£
  x ≀[ p ]' y = substα΅’ ⌞F⌟ p x ≀ y

  substα΅– : βˆ€ {i j} β†’ i ≑ᡒ j β†’ Monotone (F i) (F j)
  substα΅– reflα΅’ .hom    x   = x
  substα΅– reflα΅’ .pres-≀ x≀y = x≀y

  Disjoint-over : Displayed _ _ (Discα΅’ I)
  Disjoint-over .D.Ob[_]        = ⌞F⌟
  Disjoint-over .D.Rel[_] p x y = x ≀[ p ]' y
  Disjoint-over .D.≀-thin' _  = hlevel 1
  Disjoint-over .D.≀-refl'    = F.≀-refl
  Disjoint-over .D.≀-antisym' = F.≀-antisym
  Disjoint-over .D.≀-trans' {f = reflα΅’} {g = reflα΅’} =
    F.≀-trans

To differentiate from the binary coproducts, we refer to the indexed coproduct of a family as disjoint coproducts, or Disjoint for short.

  Disjoint : Poset _ _
  Disjoint = ∫ Disjoint-over

_≀[_]_
  : βˆ€ {β„“ ℓₐ β„“α΅£} {I : Set β„“} {F : ⌞ I ⌟ β†’ Poset ℓₐ β„“α΅£} {i j : ⌞ I ⌟}
  β†’ ⌞ F i ⌟ β†’ i ≑ᡒ j β†’ ⌞ F j ⌟
  β†’ Type β„“α΅£
_≀[_]_ {I = I} {F = F} x p y = _≀[_]'_ I F x p y
{-# DISPLAY _≀[_]'_ I F x p y = x ≀[ p ] y #-}

module _ {β„“ ℓₐ β„“α΅£} {I : Set β„“} {F : ⌞ I ⌟ β†’ Poset ℓₐ β„“α΅£} where
  private
    open module F {i : ⌞ I ⌟} = Pr (F i)

    ⌞F⌟ : ⌞ I ⌟ β†’ Type ℓₐ
    ⌞F⌟ e = ⌞ F e ⌟

  injα΅– : (i : ⌞ I ⌟) β†’ Monotone (F i) (Disjoint I F)
  injα΅– i .hom    x   = i , x
  injα΅– i .pres-≀ x≀y = reflα΅’ , x≀y

The name Disjoint is justified by the observation that each of the coprojections injα΄Ύ is actually an order embedding. This identifies each factor with its image in 

  injα΅–-is-order-embedding
    : βˆ€ i β†’ is-order-embedding (F i) (Disjoint I F) (apply (injα΅– i))
  injα΅–-is-order-embedding i .fst = injα΅– i .pres-≀
  injα΅–-is-order-embedding i .snd = biimp-is-equiv!
    (injα΅– i .pres-≀)
    Ξ» { (p , q) β†’ ≀-trans (≀-refl' (substα΅’-filler-set _ (hlevel 2) p _)) q }

To complete the construction of the coproduct, we have the following function for mapping out, by cases:

  matchα΅–
    : βˆ€ {o β„“} {R : Poset o β„“}
    β†’ (βˆ€ i β†’ Monotone (F i) R)
    β†’ Monotone (Disjoint I F) R
  matchα΅– cases .hom    (i , x)       = cases i # x
  matchα΅– cases .pres-≀ (reflα΅’ , x≀y) =
    cases _ .pres-≀ x≀y

Straightforward calculations finish the proof that has all set-indexed coproducts.

Posets-has-set-indexed-coproducts
  : βˆ€ {o β„“ ΞΊ} (I : Set ΞΊ)
  β†’ has-coproducts-indexed-by (Posets (o βŠ” ΞΊ) (β„“ βŠ” ΞΊ)) ⌞ I ⌟
Posets-has-set-indexed-coproducts I F = mk where
  mk : Indexed-coproduct (Posets _ _) F
  mk .Ξ£F = Disjoint I F
  mk .ΞΉ  = injα΅–
  mk .has-is-ic .match      = matchα΅–
  mk .has-is-ic .commute    = trivial!
  mk .has-is-ic .unique f p = ext Ξ» i x β†’ p i #β‚š x

Binary coproducts are a special case of indexed coproductsπŸ”—

βŠŽβ‰‘Disjoint-bool : βˆ€ {o β„“} (P Q : Poset o β„“) β†’ P βŠŽα΅– Q ≑ Disjoint (el! Bool) (if_then P else Q)
βŠŽβ‰‘Disjoint-bool P Q = Poset-path Ξ» where
  .to   β†’ matchβŠŽα΅– (injα΅– true) (injα΅– false)
  .from β†’ matchα΅– (Bool-elim _ inlα΅– inrα΅–)
  .inverses .invl β†’ ext Ξ» where
    true  x β†’ refl
    false x β†’ refl
  .inverses .invr β†’ ext Ξ» where
    (inl x) β†’ refl
    (inr x) β†’ refl

  1. where and β†©οΈŽ