\import Logic
\import Logic.Meta
\import Operations
\import Order.PartialOrder

\class DirectedSet \extends Preorder
  | isInhabitted : ∃ E
  | isDirected (x y : E) : ∃ (z : E) (x <= z) (y <= z)

\instance ProductDirectedSet (X Y : DirectedSet) : DirectedSet (\Sigma X Y)
  | Preorder => ProductPreorder X Y
  | isInhabitted => \case X.isInhabitted, Y.isInhabitted \with {
    | inP x, inP y => inP (x,y)
  }
  | isDirected s t => \case isDirected s. t., isDirected s. t. \with {
    | inP (x,p,q), inP (y,p',q') => inP ((x,y), (p,p'), (q,q'))
  }

\instance DirectedSetHasProduct : HasProduct DirectedSet
  | Product => ProductDirectedSet