// Preorder: a set with a reflexive, transitive relation
//
// This demonstrates RELATIONS (predicates) as opposed to functions.
// A relation R : A -> Prop is a predicate on A.
// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop

theory Preorder {
  X : Sort;

  // The ordering relation: x ≤ y
  leq : [x: X, y: X] -> Prop;

  // Reflexivity: x ≤ x
  ax/refl : forall x : X.
    |- [x: x, y: x] leq;

  // Transitivity: x ≤ y ∧ y ≤ z → x ≤ z
  ax/trans : forall x : X, y : X, z : X.
    [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
}

// The discrete preorder: only reflexive pairs
// (no elements are comparable except to themselves)
// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl.
instance Discrete3 : Preorder = chase {
  a : X;
  b : X;
  c : X;
}

// A total order on 3 elements: a ≤ b ≤ c
// Uses `chase` to derive reflexive and transitive closure.
instance Chain3 : Preorder = chase {
  bot : X;
  mid : X;
  top : X;

  // Assert the basic ordering; chase will add reflexive pairs
  // and transitive closure (bot ≤ top)
  [x: bot, y: mid] leq;
  [x: mid, y: top] leq;
}