First

.gitignore

@@ -0,0 +1 @@
+_build

Prelude.agda

@@ -0,0 +1,176 @@
+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 _≟_

prelude.agda-lib

@@ -0,0 +1,3 @@
+name: prelude
+depend: standard-library
+include: .