{-# OPTIONS --safe --cubical #-}

module OWL2.Prelude where

open import Agda.Builtin.String public
  using (String; primStringEquality; primShowString)
open import Cubical.Foundations.Prelude public
open import Cubical.Data.Bool.Base public using (Bool; true; false; if_then_else_)
open import Cubical.Data.Empty.Base public using (⊥; ⊥*)
open import Cubical.Data.List.Base public
  using (List; []; _∷_; _++_; map; filterMap; foldr)
open import Cubical.Data.List.Dependent public using (RepListP)
open import Cubical.Data.Maybe.Base public
  hiding (caseMaybe; map-Maybe; rec; elim)
  renaming (Maybe to Optional; nothing to absent; just to present)
open import Cubical.Data.Nat.Base public using (ℕ)
open import Cubical.Data.Sigma.Base public using (_×_; _,_)
open import Cubical.Data.Sum.Base public using (_⊎_; inl; inr)
open import Cubical.Data.Unit.Base public using (Unit; Unit*; tt; tt*)
open import Cubical.Relation.Binary.Base public using (Rel; module BinaryRelation)
open import Cubical.Relation.Nullary.Base public using (¬_)