\import Category
\import Category.Functor
\import Logic
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.SetHom

\class Preorder \extends BaseSet, Precat {
  | \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

  \protected \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 Is-meet (x y m : E) => \Sigma (m <= x) (m <= y) (\Pi (m' : E) -> m' <= x -> m' <= y -> m' <= m)

  \func IsJoin {J : \Set} (f : J -> E) (a : E) => \Sigma (\Pi (j : J) -> f j <= a) (\Pi {b : E} -> (\Pi (j : J) -> f j <= b) -> a <= b)

  \func IsMeet {J : \Set} (f : J -> E) (a : E) => \Sigma (\Pi (j : J) -> a <= f j) (\Pi {b : E} -> (\Pi (j : J) -> b <= f j) -> b <= a)
}

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

\lemma \infixr  =<= {E : Preorder} {x y z : E} (p : x = y) (q : y <= z) : x <= z
  => =_<= p <=∘ q

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

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

\instance TrivialPoset : Poset (\Sigma)
  | <= _ _ => \Sigma
  | <=-refl => ()
  | <=-transitive _ _ => ()
  | <=-antisymmetric _ _ => idp

\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')

\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')

\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)

\record PreorderHom \extends SetHom, Functor {
  \override Dom : Preorder
  \override Cod : Preorder

  | func-<= {x y : Dom} : x <= y -> func x <= func y

  | C => Dom
  | D => Cod
  | F => func
  | Func => func-<=
  | Func-id => prop-pi
  | Func-o => prop-pi
} \where {
  \func id {P : Preorder} : PreorderHom P P \cowith
    | func x => x
    | func-<= p => p

  \func \fixl  compose \alias \infixl  ∘ {P Q R : Preorder} (g : PreorderHom Q R) (f : PreorderHom P Q) : PreorderHom P R \cowith
    | func x => g (f x)
    | func-<= p => func-<= (func-<= p)
}

\record PosetHom \extends PreorderHom {
  \override Dom : Poset
  \override Cod : Poset
} \where {
  \func id {P : Poset} : PosetHom P P \cowith
    | func x => x
    | func-<= p => p

  \func \fixl  compose \alias \infixl  ∘ {P Q R : Poset} (g : PosetHom Q R) (f : PosetHom P Q) : PosetHom P R \cowith
    | func x => g (f x)
    | func-<= p => func-<= (func-<= p)
}