open import Cat.Prelude

open import Order.Instances.Props
open import Order.Base

module Order.Instances.Elements.Covariant where

module _ {o ℓ} {P : Poset o ℓ} where
  open Poset P

The covariant poset of elements🔗

The covariant poset of elements of an upper set denoted is the poset whose elements are the such that holds, where the order is given by the ordering of 

  ∫ : (F : Monotone P Props) → Poset o ℓ
  ∫ F .Poset.Ob = ∫ₚ F
  ∫ F .Poset._≤_ (x , _) (y , _) = x ≤ y
  ∫ F .Poset.≤-thin = hlevel 1
  ∫ F .Poset.≤-refl = ≤-refl
  ∫ F .Poset.≤-trans = ≤-trans
  ∫ F .Poset.≤-antisym x≤y y≤x = Σ-prop-path! (≤-antisym x≤y y≤x)

As the name suggests, this is the order-theoretic analog of the covariant category of elements.