--  Modules on the realizability tripos.

--  The "Prealgebra" modules establish that 𝔸-valued predicates on a set X form a Heyting prealgebra.
--  The "Syntax" and "Semantics" modules deal with the internal logic of the tripos.
module Realizability.Tripos.Everything where

open import Realizability.Tripos.Prealgebra.Everything
open import Realizability.Tripos.Logic.Syntax
open import Realizability.Tripos.Logic.Semantics