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