\import Category
\import Category.Meta
\import Function.Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths.Meta
\import Set
\import Set.SetHom

\instance PosetCat.{u} : Cat Poset.{u}
  | Hom P1 P2 => PosetHom P1 P2
  | id => PosetHom.id
  | o => PosetHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {_} {_} {_} p p1 => ext (ext (\lam _ _ => ext (\lam _x => func-<= {p} _x, \lam _x => func-<= {p1} _x)))

\record StrictPosetHom \extends SetHom {
  \override Dom : StrictPoset
  \override Cod : StrictPoset
  | func-< {x y : Dom} : x < y -> func x < func y
} \where {
  \func id {P : StrictPoset} : StrictPosetHom P P \cowith
    | func x => x
    | func-< p => p

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

\instance StrictPosetCat.{u} : Cat StrictPoset.{u}
  | Hom P1 P2 => StrictPosetHom P1 P2
  | id => StrictPosetHom.id
  | o => StrictPosetHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {_} {_} {_} p p1 => ext $ ext \lam _ _ => ext (\lam _x => func-< {p} _x, \lam _x => func-< {p1} _x)

\instance DecLinearOrderCat.{u} : Cat LinearOrder.Dec.{u}
  | Hom E1 E2 => PosetHom E1 E2
  | id => PosetHom.id
  | o => PosetHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip \lam {A} {S1} {S2} f g => ext LinearOrder.Dec {
    | < => ext \lam _ _ => ext (\lam l => LinearOrder.<=_/= (f.func-<= (LinearOrder.<_<= l)) (StrictPoset.<_/= l),
                                \lam l => LinearOrder.<=_/= (g.func-<= (LinearOrder.<_<= l)) (StrictPoset.<_/= l))
    | meet => ext \lam _ _ => S1.<=-antisymmetric (g.func-<= (meet-univ (f.func-<= meet-left) (f.func-<= meet-right))) (meet-univ (g.func-<= meet-left) (g.func-<= meet-right))
    | join => ext \lam _ _ => S2.<=-antisymmetric (f.func-<= (join-univ (g.func-<= join-left) (g.func-<= join-right))) (join-univ (f.func-<= join-left) (f.func-<= join-right))
    | # => ext \lam _ _ => ext (\lam a => nonEqualApart (Set#.apartNotEqual a),
                                \lam a => nonEqualApart (Set#.apartNotEqual a))
  }