\begin{code}
open import Prelude
open import Algebra
open import Cubical.Foundations.Everything using (isSet)

module Data.Set.Hom {ā„“} {š‘† : Type ā„“} (latt : Semilattice š‘†) (sIsSet : isSet š‘†) where


open import Data.Set.Definition
open import Data.Set.Eliminators renaming (āŸ¦_āŸ§ to ĻˆāŸ¦_āŸ§)


open Semilattice latt

module _ {A : Type a} where
\end{code}
%<*hom-ty>
\begin{code}
  āŸ¦_āŸ§ : (A ā†’ š‘†) ā†’ š’¦ A ā†’ š‘†
\end{code}
%</hom-ty>
\begin{code}
  āŸ¦ h āŸ§ = ĻˆāŸ¦ alg āŸ§
    where
    alg : Ļˆ A š‘†
    alg .fst āˆ… = Īµ
    alg .fst (x āˆ· xs āŸØ PāŸØxsāŸ© āŸ©) = h x āˆ™ PāŸØxsāŸ©
    alg .snd .c-trunc _ = sIsSet
    alg .snd .c-com x y _ xs = sym (assoc (h x) _ _) Ķ¾ cong (_āˆ™ xs) (comm (h x) _) Ķ¾ assoc (h y) _ _
    alg .snd .c-dup x _ xs = sym (assoc (h x) _ _) Ķ¾ cong (_āˆ™ xs) (idem (h x))
\end{code}