The quotient set of a preorder is a partial order (proof - wip)

OrdersAndEquivClasses.agda

module OrdersAndEquivClasses where

open import Level
open import Data.Product

-- X is the base
-- S is a set of things drawn from X
record PreOrder {l l' : Level} {X : Set l} {S : X -> Set l'} : Set (Level.suc l ⊔ l') where
 field
  _<_ : Σ X S -> Σ X S -> Set l
  reflx : {x : Σ X S} -> x < x
  trans : {x y z : Σ X S} -> x < y -> y < z -> x < z

open PreOrder

record PartialOrder {l l' : Level} {X : Set l} {S : X -> Set l'} : Set (Level.suc l ⊔ l') where
 field
  p        : PreOrder {l} {l'} {X} {S}
  _~_      : Σ X S -> Σ X S -> Set l
  antiSym  : {x y : Σ X S} -> _<_ p x y -> _<_ p y x -> x ~ y


_/_ : {l l' : Level} {X : Set l}
    -> (S : X -> Set l')
    -> (_~_ : Σ X S -> Σ X S -> Set (suc l ⊔ l'))
    -> ((Σ X S -> Set l') -> Set (suc l ⊔ l'))

_/_ {l} {l'} {X} S _~_ = \sub ->
 (a : Σ X S) -> (x : Σ X S) -> sub a × sub x -> (_~_ a x)


-- create the partial ordering for a quotient set based on a pre-order
partial_order :
  {l l' : Level}
  {X : Set l}
  {S : X -> Set l'}
  {_<_ : Σ X S -> Σ X S -> Set l}
  {_~_ : Σ X S -> Σ X S -> Set (suc l ⊔ l')}
  -> Σ (Σ X S → Set l') (S / _~_)
  -> Σ (Σ X S → Set l') (S / _~_)
  -> Set (l ⊔ l')
partial_order {l} {l'} {X} {S} {_<_} {_~_} (a , aIn) (b , bIn) =
  forall (x y : Σ X S) -> (a x × b y) -> x < y


quotientPO : {l l' : Level} {X : Set l} {S : X -> Set l'} {p : PreOrder {l} {l'} {X} {S}}
           {_~_ : Σ X S -> Σ X S -> Set (suc l ⊔ l')}
         -> PartialOrder {l ⊔ suc l'} {suc l ⊔ l'} {Σ X S → Set l'} {S / _~_}

quotientPO {l} {l'} {X} {S} {p} {~} =
  record {
    p = record
          { _<_ = partial_order {l} {l'} {X} {S} {_<_ p} {~} --  (level problem here)
          ; reflx = {!!}
          ; trans = {!!}
          }
  ; _~_ = {!!}
  ; antiSym = {!!} }