{-# OPTIONS --cubical-compatible #-}
module Class.Prelude where

open import Agda.Primitive public
  using () renaming (Set to Type; Setω to Typeω)
open import Level public
  using (Level; _⊔_; Lift; lift; 0ℓ) renaming (suc to lsuc)
module Fun where open import Function.Base public
open Fun public
  using (id; _∘_; _∘₂_; _∋_; _$_; const; constᵣ; flip; it; case_of_; _|>_)

open import Data.Empty public
  using (⊥; ⊥-elim)
open import Data.Unit public
  using (⊤; tt)
open import Data.These public
  using (These; this; that; these)
open import Data.Refinement public
  using (Refinement; _,_; value)
module Prod where open import Data.Product public
open Prod public
  using (_×_; _,_; proj₁; proj₂; Σ; ∃; ∃-syntax; -,_)
module Sum where open import Data.Sum public
open Sum public
  using (_⊎_; inj₁; inj₂)
module 𝔹 where open import Data.Bool public
open 𝔹 public
  using (Bool; true; false; not; if_then_else_; T)
module Nat where open import Data.Nat public; open import Data.Nat.Properties public
open Nat public
  using (ℕ; zero; suc)
module Bin where open import Data.Nat.Binary public
open Bin public
  using (ℕᵇ)
module Fi where open import Data.Fin public
open Fi public
  using (Fin; zero; suc)
module Int where open import Data.Integer public
open Int public
  using (ℤ; 0ℤ; 1ℤ; -_)
module Q where open import Data.Rational public
open Q public
  using (ℚ)
module Fl where open import Data.Float public
open Fl public
  using (Float)
module Ch where open import Data.Char public
open Ch public
  using (Char)
module Str where open import Data.String public
open Str public
  using (String)
module Word where open import Data.Word64 public
open Word public
  using (Word64)
module Mb where open import Data.Maybe public
open Mb public
  using (Maybe; just; nothing; maybe; fromMaybe)
module L where open import Data.List public
open L public
  using (List; []; _∷_; [_]; map; _++_; foldr; concat; concatMap; length)
module L⁺ where open import Data.List.NonEmpty public
open L⁺ public
  using (List⁺; _∷_; _⁺++⁺_; foldr₁)
module V where open import Data.Vec public
open V public
  using (Vec; []; _∷_)

module Meta where
  open import Reflection public
  open import Reflection.AST public
  open import Reflection.TCM public
open Meta public
  using (TC; Arg; Abs)

open import Relation.Nullary public
  using (¬_; Dec; yes; no; contradiction; Irrelevant)
open import Relation.Nullary.Decidable public
  using (⌊_⌋; dec-yes; isYes)
  renaming (map′ to mapDec)
open import Relation.Unary public
  using (Pred)
  renaming (Decidable to Decidable¹)
open import Relation.Binary public
  using ( REL; Rel; DecidableEquality
        ; IsEquivalence; Setoid
        )
  renaming (Decidable to Decidable²)
module _ {a b c} where
  3REL : (A : Type a) (B : Type b) (C : Type c) (ℓ : Level) → Type _
  3REL A B C ℓ = A → B → C → Type ℓ

  Decidable³ : ∀ {A B C ℓ} → 3REL A B C ℓ → Type _
  Decidable³ _~_~_ = ∀ x y z → Dec (x ~ y ~ z)
open import Relation.Binary.PropositionalEquality public
  using (_≡_; refl; sym; cong; subst; trans)

variable
  ℓ ℓ′ ℓ″ ℓ‴ : Level
  A B C : Type ℓ
  x y : A
  P Q : Pred A ℓ
  R R′ : Rel A ℓ
  n m : ℕ

module Alg (_~_ : Rel A ℓ) where
  open import Algebra.Definitions _~_ public
module Alg≡ {ℓ} {A : Type ℓ} = Alg (_≡_ {A = A})

itω : ∀ {A : Typeω} → ⦃ A ⦄ → A
itω ⦃ x ⦄ = x