module Cubical.Categories.Instances.DistLattice where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.DistLattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Lattice

open Category

DistLatticeCategory : ∀ {ℓ} (L : DistLattice ℓ) → Category ℓ ℓ
DistLatticeCategory L = LatticeCategory (DistLattice→Lattice L)