module Relation.Binary.OrderMorphism where
open import Relation.Binary
open Poset
import Data.Function as F
record _⇒-Poset_ (po₁ po₂ : Poset) : Set where
field
fun : carrier po₁ → carrier po₂
monotone : _≤_ po₁ =[ fun ]⇒ _≤_ po₂
_⇒-DTO_ : (dto₁ dto₂ : DecTotalOrder) → Set
dto₁ ⇒-DTO dto₂ = poset dto₁ ⇒-Poset poset dto₂
where open DecTotalOrder
open _⇒-Poset_
id : ∀ {po} → po ⇒-Poset po
id = record
{ fun = F.id
; monotone = F.id
}
_∘_ : ∀ {po₁ po₂ po₃} →
po₂ ⇒-Poset po₃ → po₁ ⇒-Poset po₂ → po₁ ⇒-Poset po₃
f ∘ g = record
{ fun = F._∘_ (fun f) (fun g)
; monotone = F._∘_ (monotone f) (monotone g)
}
const : ∀ {po₁ po₂} → carrier po₂ → po₁ ⇒-Poset po₂
const {po₂ = po₂} x = record
{ fun = F.const x
; monotone = F.const (refl po₂)
}