{-# OPTIONS --safe #-} module Cubical.Categories.Instances.DistLattices where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function open import Cubical.Algebra.Lattice open import Cubical.Algebra.DistLattice open import Cubical.Categories.Category open Category DistLatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ ob DistLatticesCategory = DistLattice _ Hom[_,_] DistLatticesCategory = DistLatticeHom id DistLatticesCategory {L} = idDistLatticeHom L _⋆_ DistLatticesCategory {L} {M} {N} = compDistLatticeHom L M N ⋆IdL DistLatticesCategory {L} {M} = compIdDistLatticeHom {L = L} {M} ⋆IdR DistLatticesCategory {L} {M} = idCompDistLatticeHom {L = L} {M} ⋆Assoc DistLatticesCategory {L} {M} {N} {O} = compAssocDistLatticeHom {L = L} {M} {N} {O} isSetHom DistLatticesCategory = isSetLatticeHom _ _