open import Cubical.Foundations.Prelude

module DCPO.Category (ℓi : Level) where

open import Cubical.Categories.Category

open import Cubical.Foundations.Function

open import DCPO.Base ℓi

module _ (ℓd ℓt : Level) where
  open Category hiding (_∘_)

  DCPOCategory : Category (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓd)) (ℓ-suc ℓt)) (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓd) ℓt)
  DCPOCategory .ob = DCPO ℓd ℓt
  DCPOCategory .Hom[_,_] = DCPOMorphism
  DCPOCategory .id = idᵈᶜᵖᵒ
  DCPOCategory ._⋆_ f g = g ∘ᵈᶜᵖᵒ f
  DCPOCategory .⋆IdL f = DCPOMorphism≡ refl
  DCPOCategory .⋆IdR f = DCPOMorphism≡ refl
  DCPOCategory .⋆Assoc f g h = DCPOMorphism≡ refl
  DCPOCategory .isSetHom = isSetDCPOMorphism