module Realizability.Tripos.Prealgebra.Meets.Everything where open import Realizability.Tripos.Prealgebra.Meets.Identity open import Realizability.Tripos.Prealgebra.Meets.Idempotency open import Realizability.Tripos.Prealgebra.Meets.Associativity open import Realizability.Tripos.Prealgebra.Meets.Commutativity