update to stdlib 2.0 (#11)

src/Generics/Constructions/DecEq.agda

@@ -17,7 +17,6 @@ open import Relation.Nullary.Decidable as Decidable
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary using (DecidableEquality)
-open import Relation.Nullary.Product
 
 record DecEq {l} (A : Set l) : Set l where
   field _≟_ : DecidableEquality A

src/Generics/Prelude.agda

@@ -7,7 +7,7 @@ open import Level             public using (Setω; Level; _⊔_; Lift; lift)
                                      renaming (zero to lzero; suc to lsuc)
 
 open import Relation.Binary.PropositionalEquality public
-  hiding ([_]; Extensionality; ∀-extensionality)
+  hiding ([_])
 open import Data.Nat.Base        public using (ℕ; zero; suc; _+_)
                                         renaming (_∸_ to _-_)
 open import Data.Unit            public using (⊤; tt)
@@ -20,14 +20,14 @@ open import Data.String using (String)
 
 
 open import Reflection                      public
-  hiding (var; return; _>>=_; _>>_; assocˡ; assocʳ; visibility; relevance; module Arg)
-import Reflection.Argument
-module Arg = Reflection.Argument
-open import Reflection.Argument.Information public using (ArgInfo; arg-info; visibility)
+  hiding (var; _>>=_; _>>_; assocˡ; assocʳ; visibility; relevance; module Arg)
+import Reflection.AST.Argument
+module Arg = Reflection.AST.Argument
+open import Reflection.AST.Argument.Information public using (ArgInfo; arg-info; visibility)
                                                    renaming (modality to getModality)
-open import Reflection.Argument.Modality    public using (Modality; modality)
-open import Reflection.Argument.Relevance   public using (Relevance; relevant; irrelevant)
-open import Reflection.Argument.Visibility  public using (Visibility; visible; hidden; instance′)
+open import Reflection.AST.Argument.Modality    public using (Modality; modality)
+open import Reflection.AST.Argument.Relevance   public using (Relevance; relevant; irrelevant)
+open import Reflection.AST.Argument.Visibility  public using (Visibility; visible; hidden; instance′)
 
 private variable
   m n   : ℕ
@@ -46,7 +46,7 @@ open Irr public
 < irrelevant > A = Irr A
 
 relevance : ArgInfo → Relevance
-relevance = Reflection.Argument.Modality.relevance ∘ getModality
+relevance = Reflection.AST.Argument.Modality.relevance ∘ getModality
 
 -- withAI : ArgInfo → Term → Term
 -- withAI i t with relevance i

src/Generics/Reflection.agda

@@ -13,26 +13,26 @@ open import Data.Bool.Base
 open import Data.Maybe.Base using (Maybe; just; nothing; maybe)
 open import Agda.Builtin.Reflection renaming ( primQNameEquality to _Name≈_
                                              )
-open import Reflection.Abstraction using (unAbs)
-open import Reflection.Argument    using (_⟨∷⟩_; _⟅∷⟆_)
-open import Reflection.Term hiding (Telescope; var)
+open import Reflection.AST.Abstraction using (unAbs)
+open import Reflection.AST.Argument    using (_⟨∷⟩_; _⟅∷⟆_)
+open import Reflection.AST.Term hiding (Telescope; var)
 open import Relation.Nullary using (yes; no)
 
-open import Category.Monad   as Monad
+open import Effect.Monad   as Monad
 
-import Data.List.Categorical as List
-import Data.Nat.Induction    as Nat
-import Data.Char             as C
+import Data.List.Effectful as List
+import Data.Nat.Induction  as Nat
+import Data.Char           as C
 
-open import Reflection.TypeChecking.Monad.Instances using (tcMonad)
-open import Reflection.Traversal hiding (_,_)
+open import Reflection.TCM.Instances using (tcMonad)
+open import Reflection.AST.Traversal hiding (_,_)
 
 open import Generics.Prelude
 open import Generics.Telescope
 open import Generics.Desc renaming (_,_ to _,ω_)
 import Generics.Accessibility as Accessibility
 open import Generics.HasDesc
-import Function.Identity.Categorical as Identity
+import Function.Identity.Effectful as Identity
 
 open List.TraversableM ⦃...⦄
 open Monad.RawMonad    ⦃...⦄
@@ -54,7 +54,7 @@ liftN (suc n) f zero    = zero
 liftN (suc n) f (suc k) = suc (liftN n f k)
 
 mapVars : (ℕ → ℕ) → Term → Term
-mapVars f = traverseTerm Identity.applicative actions (0 Reflection.Traversal., [])
+mapVars f = traverseTerm Identity.applicative actions (0 Reflection.AST.Traversal., [])
   where
     actions : Actions Identity.applicative
     actions .onVar  ctx = liftN (ctx .Cxt.len) f

src/Generics/Telescope/Equality.agda

@@ -21,10 +21,6 @@ private
 -- Helpers
 
 private
-  J : ∀ {a b} {A : Set a} {x : A} (B : ∀ y → x ≡ y → Set b)
-      {y : A} (p : x ≡ y) → B x refl → B y p
-  J B refl b = b
-
   J⁻¹ : ∀ {a b} {A : Set a} {x : A} (B : ∀ y → x ≡ y → Set b)
       → {y : A} (p : x ≡ y) → B y p → B x refl
   J⁻¹ B p = J (λ y e → B y e → B _ refl) p id