module Realizability.Tripos.Prealgebra.Everything where open import Realizability.Tripos.Prealgebra.Predicate open import Realizability.Tripos.Prealgebra.Joins.Everything open import Realizability.Tripos.Prealgebra.Meets.Everything open import Realizability.Tripos.Prealgebra.Implication