{-# OPTIONS --safe #-} module Cubical.Categories.Instances.Lattice where open import Cubical.Foundations.Prelude open import Cubical.Algebra.Lattice open import Cubical.Categories.Category open import Cubical.Categories.Instances.Semilattice open Category LatticeCategory : ∀ {ℓ} (L : Lattice ℓ) → Category ℓ ℓ LatticeCategory L = JoinSemilatticeCategory (Lattice→JoinSemilattice L)