module Realizability.PERs.Everything where open import Realizability.PERs.PER open import Realizability.PERs.ResizedPER open import Realizability.PERs.SubQuotient