module Prelude where

open import Function public

open import Agda.Primitive public using (Level ; lzero ; lsuc ; _⊔_)
open import Level public using (Lift ; lift ; lower)
instance liftᴵ : ∀ {a ℓ} {A : Set a} → ⦃ A ⦄ → Lift ℓ A
liftᴵ = lift it

open import Agda.Builtin.FromNat public
open import Agda.Builtin.FromNeg public
open import Agda.Builtin.FromString public

module ⊤ where
  open import Data.Unit public hiding (module ⊤)
  open import Data.Unit.Properties public
open ⊤ public using (⊤ ; tt)

module ⊥ where
  open import Data.Empty public hiding (module ⊥ ; ⊥-elim)
  open import Data.Empty.Irrelevant public
open ⊥ public using (⊥ ; ⊥-elim)

module ℕ where
  open import Data.Nat public hiding (module ℕ)
  open import Data.Nat.Properties public
  import Data.Nat.Literals as Lit

  instance number = Lit.number
open ℕ public using (ℕ ; zero ; suc)

module Fin where
  import Data.Fin hiding (module Fin)
  open Data.Fin public
  open import Data.Fin.Properties public
  import Data.Fin.Literals as Lit

  instance number : ∀ {n} → Number (Fin n)
  number = Lit.number _
open Fin public using (Fin ; zero ; suc ; #_)

module Bool where
  open import Data.Bool public hiding (module Bool)
  open import Data.Bool.Properties public
open Bool public using (Bool ; true ; false ; if_then_else_)

module ⊎ where
  open import Data.Sum public hiding (module _⊎_)
  open import Data.Sum.Properties public
open ⊎ public using (_⊎_ ; inj₁ ; inj₂)

module Σ where
  open import Data.Product public hiding (module Σ)
  open import Data.Product.Properties public
open Σ public using (Σ ; Σ-syntax ; _×_ ; ∃ ; ∃-syntax ; ∄ ; ∄-syntax ;
                     _,_ ; -,_ ; proj₁ ; proj₂)

module List where
  open import Data.List public hiding (module List)
  open import Data.List.Properties public
open List public using (List ; [] ; _∷_)

module Vec where
  open import Data.Vec public hiding (module Vec)
  open import Data.Vec.Properties public
open Vec public using (Vec ; [] ; _∷_)

module Maybe where
  open import Data.Maybe public hiding (module Maybe)
  open import Data.Maybe.Properties public
open Maybe public using (Maybe ; nothing ; just)

module Rel where
  open import Relation.Nullary public renaming (Irrelevant to Irrelevant₀)
  open import Relation.Nullary.Decidable public
  open import Relation.Unary public hiding (⌊_⌋)
    renaming (Irrelevant to Irrelevant₁ ; Recomputable to Recomputable₁ ;
              Universal to Universal₁ ; Decidable to Decidable₁ ; _⇒_ to _⇒₁_)
  open import Relation.Binary public
    renaming (Irrelevant to Irrelevant₂ ; Recomputable to Recomputable₂ ;
              Universal to Universal₂ ; Decidable to Decidable₂ ; _⇒_ to _⇒₂_)

  module _ where
    private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ : Level ; A B C D E F G : Set _

    _Preserves₃_⟶_⟶_⟶_ :
      (A → B → C → D) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Rel D ℓ₄ → Set _
    f Preserves₃ _∼ᵃ_ ⟶ _∼ᵇ_ ⟶ _∼ᶜ_ ⟶ _∼ᵈ_ =
      ∀ {a a′ b b′ c c′} →
      a ∼ᵃ a′ → b ∼ᵇ b′ → c ∼ᶜ c′ →
      f a b c ∼ᵈ f a′ b′ c′

    _Preserves₄_⟶_⟶_⟶_⟶_ :
      (A → B → C → D → E) →
      Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Rel D ℓ₄ → Rel E ℓ₅ → Set _
    f Preserves₄ _∼ᵃ_ ⟶ _∼ᵇ_ ⟶ _∼ᶜ_ ⟶ _∼ᵈ_ ⟶ _∼ᵉ_ =
      ∀ {a a′ b b′ c c′ d d′} →
      a ∼ᵃ a′ → b ∼ᵇ b′ → c ∼ᶜ c′ → d ∼ᵈ d′ →
      f a b c d ∼ᵉ f a′ b′ c′ d′

    _Preserves₅_⟶_⟶_⟶_⟶_⟶_ :
      (A → B → C → D → E → F) →
      Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Rel D ℓ₄ → Rel E ℓ₅ → Rel F ℓ₆ → Set _
    f Preserves₅ _∼ᵃ_ ⟶ _∼ᵇ_ ⟶ _∼ᶜ_ ⟶ _∼ᵈ_ ⟶ _∼ᵉ_ ⟶ _∼ᶠ_ =
      ∀ {a a′ b b′ c c′ d d′ e e′} →
      a ∼ᵃ a′ → b ∼ᵇ b′ → c ∼ᶜ c′ → d ∼ᵈ d′ → e ∼ᵉ e′ →
      f a b c d e ∼ᶠ f a′ b′ c′ d′ e′

    _Preserves₆_⟶_⟶_⟶_⟶_⟶_⟶_ :
      (A → B → C → D → E → F → G) →
      Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Rel D ℓ₄ → Rel E ℓ₅ → Rel F ℓ₆ →
      Rel G ℓ₇ → Set _
    𝑓 Preserves₆ _∼ᵃ_ ⟶ _∼ᵇ_ ⟶ _∼ᶜ_ ⟶ _∼ᵈ_ ⟶ _∼ᵉ_ ⟶ _∼ᶠ_ ⟶ _∼ᵍ_ =
      ∀ {a a′ b b′ c c′ d d′ e e′ f f′} →
      a ∼ᵃ a′ → b ∼ᵇ b′ → c ∼ᶜ c′ → d ∼ᵈ d′ → e ∼ᵉ e′ → f ∼ᶠ f′ →
      𝑓 a b c d e f ∼ᵍ 𝑓 a′ b′ c′ d′ e′ f′

open Rel public
  using (Dec ; yes ; no ; ¬_ ; True ; False ; ⌊_⌋ ;
         Pred ; Decidable₁ ; Rel ; Decidable₂)

open import Algebra.Core public
module Algebra where
  open import Algebra.Definitions as D public
  open import Algebra.Structures  as S public
  open import Algebra.Bundles     as B public

  module WithEq {a ℓ} {A : Set a} (≈ : Rel A ℓ) where
    open D ≈ public
    open S ≈ public
    open B public

module ≡ where
  open import Relation.Binary.PropositionalEquality public hiding (module _≡_)

  At : ∀ {a} (A : Set a) → Rel A _
  At A = _≡_ {A = A}
open ≡ public using (_≡_ ; _≢_ ; refl) renaming (At to ≡-At)


record Eq {a} (A : Set a) : Set a where
  field _≟_ : Decidable₂ $ ≡-At A
open Eq ⦃ … ⦄ public

module _ where
  private variable a b : Level ; A : Set a ; B : Set b ; F : A → Set b ; n : ℕ
  instance
    eq-⊤ : Eq ⊤
    eq-⊤ ._≟_ = ⊤._≟_

    eq-⊥ : Eq ⊥
    eq-⊥ ._≟_ () ()

    eq-ℕ : Eq ℕ
    eq-ℕ ._≟_ = ℕ._≟_

    eq-fin : Eq (Fin n)
    eq-fin ._≟_ = Fin._≟_

    eq-bool : Eq Bool
    eq-bool ._≟_ = Bool._≟_

    eq-⊎ : ⦃ Eq A ⦄ → ⦃ Eq B ⦄ → Eq (A ⊎ B)
    eq-⊎ ._≟_ = ⊎.≡-dec _≟_ _≟_

    eq-prod : ⦃ Eq A ⦄ → ⦃ Rel.∀[ Eq ∘ F ] ⦄ → Eq (Σ A F)
    eq-prod ._≟_ = Σ.≡-dec _≟_ _≟_

    eq-maybe : ⦃ Eq A ⦄ → Eq (Maybe A)
    eq-maybe ._≟_ = Maybe.≡-dec _≟_

    eq-list : ⦃ Eq A ⦄ → Eq (List A)
    eq-list ._≟_ = List.≡-dec _≟_

    eq-vec : ⦃ Eq A ⦄ → Eq (Vec A n)
    eq-vec ._≟_ = Vec.≡-dec _≟_