move imports for agda-stdlib 1.3
[~helmut/bidiragda.git] / Bidir.agda
index e31d844..580b770 100644 (file)
@@ -15,9 +15,9 @@ open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing ; drop-ju
 open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_)
 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_)
 open import Data.List using (List)
-open import Data.List.All using (All)
+open import Data.List.Relation.Unary.All using (All)
 open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; allFin) renaming (lookup to lookupVec)
-open import Data.Vec.Relation.Pointwise.Inductive using (Pointwise)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
 open import Data.Vec.Properties using (lookup∘tabulate ; lookup∘update ; map-cong ; map-∘ ; map-lookup-allFin)
 open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂)
 open import Function using (id ; _∘_ ; flip)
@@ -25,7 +25,7 @@ open import Relation.Binary.Indexed.Heterogeneous using () renaming (IndexedSeto
 open import Relation.Binary.Indexed.Heterogeneous.Construct.At using (_atₛ_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_ ; inspect ; [_] ; module ≡-Reasoning)
 open import Relation.Binary using (Setoid ; module Setoid ; module DecSetoid)
-import Relation.Binary.EqReasoning as EqR
+import Relation.Binary.Reasoning.Setoid as EqR
 
 open import Structures using (Functor ; IsFunctor ; Shaped ; module Shaped)
 open import Instances using (MaybeFunctor ; ShapedISetoid)
@@ -66,21 +66,21 @@ _in-domain-of_ : {m n : ℕ} {A : Set} → (is : Vec (Fin m) n) → (FinMapMaybe
 _in-domain-of_ is h = All (λ i → ∃ λ x → lookupM i h ≡ just x) (toList is)
 
 lemma-assoc-domain : {m n : ℕ} → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → is in-domain-of h
-lemma-assoc-domain []         []         ph = Data.List.All.[]
+lemma-assoc-domain []         []         ph = Data.List.Relation.Unary.All.[]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph with assoc is' xs' | inspect (assoc is') xs'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | nothing | [ ph' ]
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') ph | just h' | [ ph' ] with checkInsert i' x' h' | inspect (checkInsert i' x') h' | insertionresult i' x' h'
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h | [ ph' ] | ._ | _ | same x _ pl = All._∷_ (x , pl) (lemma-assoc-domain is' xs' ph')
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') P.refl | just h' | [ ph' ] | ._ | [ cI≡ ] | new _ = All._∷_
   (x' , lookup∘update i' h' (just x'))
-  (Data.List.All.map
+  (Data.List.Relation.Unary.All.map
     (λ {i} p → proj₁ p , lemma-lookupM-checkInsert i i' h' (proj₂ p) x' cI≡)
     (lemma-assoc-domain is' xs' ph'))
 lemma-assoc-domain (i' ∷ is') (x' ∷ xs') () | just h' | [ ph' ] | ._ | _ | wrong _ _ _
 
 lemma-map-lookupM-assoc : {m : ℕ} → (i : Fin m) → (x : Carrier) → (h : FinMapMaybe m Carrier) → {h' : FinMapMaybe m Carrier} → checkInsert i x h ≡ just h' → {n : ℕ} → (js : Vec (Fin m) n) → js in-domain-of h → map (flip lookupM h') js ≡ map (flip lookupM h) js
 lemma-map-lookupM-assoc i x h ph [] pj = P.refl
-lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.All._∷_ (x' , pl) pj) = P.cong₂ _∷_
+lemma-map-lookupM-assoc i x h ph (j ∷ js) (Data.List.Relation.Unary.All._∷_ (x' , pl) pj) = P.cong₂ _∷_
   (P.trans (lemma-lookupM-checkInsert j i h pl x ph) (P.sym pl))
   (lemma-map-lookupM-assoc i x h ph js pj)