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