{-# OPTIONS --type-in-type --allow-unsolved-metas #-}

module Posets where

open import Base

-- we could just define equality to be pointwise instead of using
-- extensionality and \==, right?
postulate funext : {X Y : Set} → {f g : X → Y} → ((x : X) → f x ≡ g x) → f ≡ g

record Poset : Set where
  field
    car : Set
    _≤_ : car → car → Set
    ≤refl : {x : car} → x ≤ x
    ≤trans : {x y z : car} → x ≤ y → y ≤ z → x ≤ z
    ≤antisym : {x y : car} → x ≤ y → y ≤ x → x ≡ y

module Poset-Reasoning (X : Poset) where
  open Poset X
  eq2≤refl : {f g : car} → f ≡ g → f ≤ g
  eq2≤refl {f} {g} refl = ≤refl

  infix   _≤∎
  infixr  _≤⟨⟩_ step-≤ step-≦
  infix   ≤begin_

  ≤begin_ : {x y : car} → x ≤ y → x ≤ y
  ≤begin_ x≤y = x≤y

  _≤⟨⟩_ : (x {y} : car) → x ≤ y → x ≤ y
  _ ≤⟨⟩ x≤y = x≤y

  step-≤ : (x {y z} : car) → y ≤ z → x ≤ y → x ≤ z
  step-≤ _ y≤z x≤y = ≤trans x≤y y≤z

  step-≦ : (x {y z} : car) → y ≤ z → x ≡ y → x ≤ z
  step-≦ x y≤z x≡y = ≤trans (eq2≤refl x≡y) y≤z

  _≤∎ : (x : car) → x ≤ x
  _≤∎ _ = ≤refl

  syntax step-≤ x y≤z x≤y = x ≤⟨ x≤y ⟩ y≤z
  syntax step-≦ x y≤z x≡y = x ≦⟨ x≡y ⟩ y≤z


trivialPoset : Poset
trivialPoset = record
                { car = ⊤
                ; _≤_ = λ tt tt → ⊤
                ; ≤refl = tt
                ; ≤trans = λ _ _ → tt
                ; ≤antisym = λ _ _ → refl
                }

record _→ₘ_ (X Y : Poset) : Set where
  constructor _!_
  private
    module X = Poset X
    module Y = Poset Y

  field
    fun : X.car → Y.car
    monot : {x x' : X.car} → x X.≤ x' → fun x Y.≤ fun x'
open _→ₘ_

postulate →ₘeq : {X Y : Poset} → {f g : X →ₘ Y} → fun f ≡ fun g → f ≡ g

_→ₘ,≤_ : (X Y : Poset) → Poset
_→ₘ,≤_ X Y = let module X = Poset X
                 module Y = Poset Y in record
  { car = X →ₘ Y 
  ; _≤_ =  λ (f ! fm) (g ! gm) → (x : X.car) → f x Y.≤ g x
  ; ≤refl = λ _ → Y.≤refl
  ; ≤trans = λ f g x → Y.≤trans (f x) (g x)
  ; ≤antisym = {!!}
  }

PosetC : ParamCategory Poset
PosetC = let open Poset in record
         { hom = λ X Y → X →ₘ Y
         ; id = λ X → (λ x → x) ! (λ p → p)
         ; _▷_ = λ (f ! fm) (g ! gm) → (λ x → g (f x)) ! (λ p → gm (fm p))
         ; _≤_ = λ {X} {Y} (f ! fm) (g ! gm) → (x : car X) → _≤_ Y (f x) (g x)
         ; ▷lunit = refl
         ; ▷runit = refl
         ; ▷assoc = refl
         ; ≤refl =  λ {X} {Y} {(f ! fm)} → λ x → ≤refl Y 
         ; ≤trans = λ {X} {Y} {(f ! fm)} {(g ! gm)} {(h ! hm)} fgw ghw x →
                    ≤trans Y (fgw x) (ghw x)
         ; ≤antisym = λ {X} {Y} {(f ! fm)} {(g ! gm)} fg gf → →ₘeq (funext {car X} {car Y} {f} {g}
                    (λ x → ≤antisym Y (fg x) (gf x)))
         ; ▷monot≤ = λ {X} {Y} {Z} {(f ! fm) (f' ! f'm) (g ! gm) (g' ! g'm)}
                    ff' gg' x → ≤trans Z (gm (ff' x)) (gg' (f' x))
         }