\import Category
\import Function.Meta ($)
\import Logic
\import Paths.Meta
\import Relation.Equivalence
\import Set

\class Preorder \extends BaseSet, Precat (\lp,\lp) {
  | \infix  <= : E -> E -> \Prop
  | <=-refl {x : E} : x <= x
  | <=-transitive \alias \infixr  <=∘ {x y z : E} : x <= y -> y <= z -> x <= z

  | Ob => E
  | Hom => <=
  | id _ => <=-refl
  | o f g => g <=∘ f
  | id-left => prop-pi
  | id-right => prop-pi
  | o-assoc => prop-pi

  | \infix  >= : E -> E -> \Prop
  | >= x y => y <= x

  \lemma =_<= {x y : E} (p : x = y) : x <= y
    | idp => <=-refl

  \func op : Preorder E \cowith
    | <= x y => y <= x
    | <=-refl => <=-refl
    | <=-transitive p q => <=-transitive q p

  \func EquivRel : Equivalence E \cowith
    | ~ x y => \Sigma (x <= y) (y <= x)
    | ~-reflexive {x} => (<=-refl, <=-refl)
    | ~-symmetric {x} {y} x~y => (x~y., x~y.)
    | ~-transitive {x} {y} {z} x~y y~z => (x~y. <=∘ y~z., y~z. <=∘ x~y.)

  \func PreorderC => Quotient (EquivRel.~)

  \instance PosetC : Poset PreorderC
    | <= => <=C
    | <=-refl => <=C-reflexive
    | <=-transitive => <=C-transitive
    | <=-antisymmetric => <=C-antisymmetric
  \where {
    \func \infix  <=C (x y : PreorderC) : \Prop \elim x, y
      | in~ x, in~ y => x <= y
      | ~-equiv x x' x~x', in~ y => propExt (<=-transitive x~x'.) (<=-transitive {_} {x} {x'} {y} x~x'.)
      | in~ x, ~-equiv y y' y~y' => propExt (<=-transitive __ y~y'.) (<=-transitive {_} {x} __ y~y'.)

    \lemma <=C-reflexive {x : PreorderC} : x <=C x \elim x
      | in~ x => <=-refl

    \lemma <=C-transitive {x y z : PreorderC} (x<=y : x <=C y) (y<=z : y <=C z) : x <=C z \elim x, y, z
      | in~ x, in~ y, in~ z => <=-transitive x<=y y<=z

    \lemma <=C-antisymmetric {x y : PreorderC} (x<=y : x <=C y) (y<=x : y <=C x) : x = y \elim x, y
      | in~ x, in~ y => path (~-equiv x y (x<=y, y<=x))
  }

  \func IsMeet (x y m : E) => \Sigma (m <= x) (m <= y) (\Pi (m' : E) -> m' <= x -> m' <= y -> m' <= m)
}

\class Poset \extends Preorder, Cat (\lp,\lp) {
  | <=-antisymmetric {x y : E} : x <= y -> y <= x -> x = y
  | univalence => Cat.makeUnivalence \lam (e : Iso) => (<=-antisymmetric e.f e.hinv, prop-pi)

  \func op : Poset \cowith
    | Preorder => Preorder.op
    | <=-antisymmetric p q => <=-antisymmetric q p

  \lemma <=_= {x y : E} (p : x = y) : x <= y
    | idp => <=-refl
}

\instance ProductPoset (P Q : Poset) : Poset (\Sigma P Q)
  | Preorder => ProductPreorder P Q
  | <=-antisymmetric (p,q) (p',q') => ext (<=-antisymmetric p p', <=-antisymmetric q q')

\instance ProductPreorder (P Q : Preorder) : Preorder (\Sigma P Q)
  | <= (x,y) (x',y') => \Sigma (x <= x') (y <= y')
  | <=-refl => (<=-refl, <=-refl)
  | <=-transitive (p,q) (p',q') => (<=-transitive p p', <=-transitive q q')

\func subPoset {P : Poset} (S : P -> \Prop) : Poset (\Sigma (x : P) (S x)) \cowith
  | <= x y => x. <= y.
  | <=-refl => <=-refl
  | <=-transitive => <=-transitive
  | <=-antisymmetric p q => ext (<=-antisymmetric p q)