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