open import 1Lab.Type using (⊥)

open import Cat.Diagram.Coproduct
open import Cat.Diagram.Initial
open import Cat.Prelude

open import Data.Set.Truncation
open import Data.Id.Base
open import Data.Sum

open import Order.Base

import Order.Reasoning as Pr

open is-coproduct
open Coproduct
open Initial

module Order.Instances.Coproduct where

Coproducts of posets🔗

If we’re given two partially ordered sets $P,Q\text{,}$ then there is a universal way of equipping their coproduct (at the level of sets) with a partial order, which results in the categorical coproduct in the category $\mathbf{Pos}\text{.}$

module _ {o o' ℓ ℓ'} (P : Poset o ℓ) (Q : Poset o' ℓ') where
  private
    module P = Pr P
    module Q = Pr Q

The ordering is defined by recursion, and it’s uniquely specified by saying that it is the coproduct of orders, and that each coprojection is an order embedding. We compute:

    sum-≤ : ⌞ P ⌟ ⊎ ⌞ Q ⌟ → ⌞ P ⌟ ⊎ ⌞ Q ⌟ → Type (ℓ ⊔ ℓ')
    sum-≤ (inl x) (inl y) = Lift ℓ' (x P.≤ y)
    sum-≤ (inl x) (inr y) = Lift _ ⊥
    sum-≤ (inr x) (inl y) = Lift _ ⊥
    sum-≤ (inr x) (inr y) = Lift ℓ (x Q.≤ y)

    abstract
      sum-≤-thin : ∀ {x y} → is-prop (sum-≤ x y)
      sum-≤-thin {inl x} {inl y} = hlevel 
      sum-≤-thin {inr x} {inr y} = hlevel 

      sum-≤-refl : ∀ {x} → sum-≤ x x
      sum-≤-refl {inl x} = lift P.≤-refl
      sum-≤-refl {inr x} = lift Q.≤-refl

      sum-≤-trans : ∀ {x y z} → sum-≤ x y → sum-≤ y z → sum-≤ x z
      sum-≤-trans {inl x} {inl y} {inl z} (lift p) (lift q) = lift (P.≤-trans p q)
      sum-≤-trans {inr x} {inr y} {inr z} (lift p) (lift q) = lift (Q.≤-trans p q)

      sum-≤-antisym : ∀ {x y} → sum-≤ x y → sum-≤ y x → x ≡ y
      sum-≤-antisym {inl x} {inl y} (lift p) (lift q) = ap inl (P.≤-antisym p q)
      sum-≤-antisym {inr x} {inr y} (lift p) (lift q) = ap inr (Q.≤-antisym p q)

  _⊎ᵖ_ : Poset (o ⊔ o') (ℓ ⊔ ℓ')
  _⊎ᵖ_ .Poset.Ob        = P.Ob ⊎ Q.Ob
  _⊎ᵖ_ .Poset._≤_       = sum-≤
  _⊎ᵖ_ .Poset.≤-thin    = sum-≤-thin
  _⊎ᵖ_ .Poset.≤-refl    = sum-≤-refl
  _⊎ᵖ_ .Poset.≤-trans   = sum-≤-trans
  _⊎ᵖ_ .Poset.≤-antisym = sum-≤-antisym

  infixr  _⊎ᵖ_

module _ {o o' ℓ} {P : Poset o ℓ} {Q : Poset o' ℓ} where

As usual, we have two (monotone) coprojections $P\to P\uplus Q$ and $Q\to P\uplus Q\text{;}$ and, if we have maps $P\to R$ and $Q\to R\text{,}$ we can define a map out of the coproduct by cases:

  inlᵖ : Monotone P (P ⊎ᵖ Q)
  inlᵖ .hom        = inl
  inlᵖ .pres-≤ x≤y = lift x≤y

  inrᵖ : Monotone Q (P ⊎ᵖ Q)
  inrᵖ .hom        = inr
  inrᵖ .pres-≤ x≤y = lift x≤y

  matchᵖ : ∀ {o ℓ} {R : Poset o ℓ} → Monotone P R → Monotone Q R → Monotone (P ⊎ᵖ Q) R
  matchᵖ f g .hom (inl x) = f # x
  matchᵖ f g .hom (inr x) = g # x
  matchᵖ f g .pres-≤ {inl x} {inl y} (lift α) = f .pres-≤ α
  matchᵖ f g .pres-≤ {inr x} {inr y} (lift β) = g .pres-≤ β

A straightforward calculation shows that this really is the coproduct in $\mathbf{Pos}\text{.}$

Posets-has-coproducts : ∀ {o ℓ} → has-coproducts (Posets o ℓ)
Posets-has-coproducts P Q .coapex = P ⊎ᵖ Q
Posets-has-coproducts P Q .ι₁ = inlᵖ
Posets-has-coproducts P Q .ι₂ = inrᵖ
Posets-has-coproducts P Q .has-is-coproduct .is-coproduct.[_,_] = matchᵖ
Posets-has-coproducts P Q .has-is-coproduct .[]∘ι₁ = trivial!
Posets-has-coproducts P Q .has-is-coproduct .[]∘ι₂ = trivial!
Posets-has-coproducts P Q .has-is-coproduct .unique α β = ext λ where
  (inl x) → α #ₚ x
  (inr x) → β #ₚ x

As a related fact, we can show that the empty poset is the initial object in $\mathbf{Pos}\text{.}$

Posets-initial : ∀ {o ℓ} → Initial (Posets o ℓ)
Posets-initial .bot = 𝟘ᵖ
Posets-initial .has⊥ P .centre .hom    ()
Posets-initial .has⊥ P .centre .pres-≤ ()
Posets-initial .has⊥ P .paths f = ext λ ()