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