{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

module prelude where

open import dtt public
open import InteractionSystems public