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

open import Data.Bool
open import Data.Sum

open import Order.Instances.LexicalSum
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 ⌟

The indexed coproduct is a special case of the lexicographic sum where the base poset is discrete. It means that there is no non-trivial relationship across fibres.

  Disjoint : Poset _ _
  Disjoint = Lexical-sum (Discα΅’ I) F

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α΅– = lexical-sum-injα΅– {I = Discα΅’ I} {F = F}

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 =
    lexical-sum-injα΅–-is-order-embedding {I = Discα΅’ I} {F = F}

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 reflα΅’)

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