{-# OPTIONS --type-in-type
#-}
open import NeilPrelude
module PartialOrder {A : Set} (_≤_ : Rel A)
(reflex : Reflexive _≤_)
(antisym : Antisymmetric _≤_)
(transit : Transitive _≤_)
where
import PreOrder
open PreOrder _≤_ reflex transit public
antisymmetric : Antisymmetric _≤_
antisymmetric = antisym