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

\class Preorder \extends BaseSet, Precat (\lp,\lp) {
| \infix 4 <= : E -> E -> \Prop
| <=-refl {x : E} : x <= x
| <=-transitive \alias \infixr 9 <=∘ {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 4 >= : 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.2, x~y.1)
| ~-transitive {x} {y} {z} x~y y~z => (x~y.1 <=∘ y~z.1, y~z.2 <=∘ x~y.2)

\func PreorderC => Quotient (EquivRel.~)

\instance PosetC : Poset PreorderC
| <= => <=C
| <=-refl => <=C-reflexive
| <=-transitive => <=C-transitive
| <=-antisymmetric => <=C-antisymmetric
\where {
\func \infix 4 <=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'.2) (<=-transitive {_} {x} {x'} {y} x~x'.1)
| in~ x, ~-equiv y y' y~y' => propExt (<=-transitive __ y~y'.1) (<=-transitive {_} {x} __ y~y'.2)

\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.1 <= y.1
| <=-refl => <=-refl
| <=-transitive => <=-transitive
| <=-antisymmetric p q => ext (<=-antisymmetric p q)```