```------------------------------------------------------------------------
-- Order morphisms
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Relation.Binary.OrderMorphism where

open import Relation.Binary
open Poset
import Function as F
open import Level

record _⇒-Poset_ {p₁ p₂ p₃ p₄ p₅ p₆}
(P₁ : Poset p₁ p₂ p₃)
(P₂ : Poset p₄ p₅ p₆) : Set (p₁ ⊔ p₃ ⊔ p₄ ⊔ p₆) where
field
fun      : Carrier P₁ → Carrier P₂
monotone : _≤_ P₁ =[ fun ]⇒ _≤_ P₂

_⇒-DTO_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
DecTotalOrder p₁ p₂ p₃ →
DecTotalOrder p₄ p₅ p₆ → Set _
DTO₁ ⇒-DTO DTO₂ = poset DTO₁ ⇒-Poset poset DTO₂
where open DecTotalOrder

open _⇒-Poset_

id : ∀ {p₁ p₂ p₃} {P : Poset p₁ p₂ p₃} → P ⇒-Poset P
id = record
{ fun      = F.id
; monotone = F.id
}

_∘_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆ p₇ p₈ p₉}
{P₁ : Poset p₁ p₂ p₃}
{P₂ : Poset p₄ p₅ p₆}
{P₃ : Poset p₇ p₈ p₉} →
P₂ ⇒-Poset P₃ → P₁ ⇒-Poset P₂ → P₁ ⇒-Poset P₃
f ∘ g = record
{ fun      = F._∘_ (fun f)      (fun g)
; monotone = F._∘_ (monotone f) (monotone g)
}

const : ∀ {p₁ p₂ p₃ p₄ p₅ p₆}
{P₁ : Poset p₁ p₂ p₃}
{P₂ : Poset p₄ p₅ p₆} →
Carrier P₂ → P₁ ⇒-Poset P₂
const {P₂ = P₂} x = record
{ fun      = F.const x
; monotone = F.const (refl P₂)
}
```