open import 1Lab.Type using (βŠ₯)

open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
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-product
open Terminal
open Product

module Order.Instances.Product where

Products of posetsπŸ”—

Specialising the construction of pointwise orderings, we can show that the product of two partial orders is given by equipping the product of their underlying sets with an ordering given on components:

_Γ—α΅–_ : βˆ€ {o o' β„“ β„“'} β†’ Poset o β„“ β†’ Poset o' β„“' β†’ Poset (o βŠ” o') (β„“ βŠ” β„“')
P Γ—α΅– Q = po module Γ—α΅– where
  module P = Pr P
  module Q = Pr Q

  po : Poset _ _
  po .Poset.Ob = P.Ob Γ— Q.Ob
  po .Poset._≀_ (x , x') (y , y') = x P.≀ y Γ— x' Q.≀ y'
  po .Poset.≀-thin = hlevel 1
  po .Poset.≀-refl = P.≀-refl , Q.≀-refl
  po .Poset.≀-trans   (f≀g , f≀g') (g≀h , g≀h') =
    P.≀-trans f≀g g≀h , Q.≀-trans f≀g' g≀h'
  po .Poset.≀-antisym (f≀g , f≀g') (g≀f , g≀f') = ext $
    P.≀-antisym f≀g g≀f , Q.≀-antisym f≀g' g≀f'

{-# DISPLAY Γ—α΅–.po a b = a Γ—α΅– b #-}
infixr 20 _Γ—α΅–_


module _ {o o' β„“ β„“'} {P : Poset o β„“} {Q : Poset o' β„“'} where

  fstα΅– : Monotone (P Γ—α΅– Q) P
  fstα΅– .hom    = fst
  fstα΅– .pres-≀ = fst

  sndα΅– : Monotone (P Γ—α΅– Q) Q
  sndα΅– .hom    = snd
  sndα΅– .pres-≀ = snd

  pairα΅–
    : βˆ€ {o β„“} {R : Poset o β„“}
    β†’ Monotone R P
    β†’ Monotone R Q
    β†’ Monotone R (P Γ—α΅– Q)
  pairα΅– f g .hom      x = f # x , g # x
  pairα΅– f g .pres-≀ x≀y = f .pres-≀ x≀y , g .pres-≀ x≀y

It’s straightforward to show this really is the product in 

Posets-has-products : βˆ€ {o β„“} β†’ has-products (Posets o β„“)
Posets-has-products P Q .apex = P Γ—α΅– Q
Posets-has-products P Q .π₁ = fstα΅–
Posets-has-products P Q .Ο€β‚‚ = sndα΅–
Posets-has-products P Q .has-is-product .⟨_,_⟩     = pairα΅–
Posets-has-products P Q .has-is-product .Ο€β‚βˆ˜factor = trivial!
Posets-has-products P Q .has-is-product .Ο€β‚‚βˆ˜factor = trivial!
Posets-has-products P Q .has-is-product .unique other Ξ± Ξ² =
  ext Ξ» x β†’ Ξ± #β‚š x , Ξ² #β‚š x

As a related observation, we can show that the unique partial order on the set with one element is the terminal object in 

Posets-terminal : βˆ€ {o β„“} β†’ Terminal (Posets o β„“)
Posets-terminal .top = πŸ™α΅–
Posets-terminal .has⊀ P .centre .hom    _ = lift tt
Posets-terminal .has⊀ P .centre .pres-≀ _ = lift tt
Posets-terminal .has⊀ P .paths f = trivial!