port to agda/2.6.0.1 and agda-stdlib/1.1

 * Data.Vec.lookup changed parameter order.
 * A number of symbols were moved from Data.Maybe to submodules.
 * In a number of occasions, agda no longer figures implicit arguments
   and they had to be made explicit.
 * We can no longer use heterogeneous proofs inside equational reasoning
   for propositional equality. Use heterogeneous equational reasoning.
 * Stop importing proof-irrelevance as that would require K.

1 files changed, 5 insertions, 3 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 64f6d1b..e31d844 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -8,8 +8,10 @@ open import Data.Fin using (Fin)
 import Level
 import Category.Monad
 import Category.Functor
-open import Data.Maybe using (Maybe ; nothing ; just ; maybe′ ; drop-just ; just-injective) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
+open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
 import Data.Maybe.Categorical
+open import Data.Maybe.Properties using (just-injective)
+open import Data.Maybe.Relation.Binary.Pointwise using (just ; nothing ; drop-just) renaming (setoid to MaybeSetoid ; Pointwise to MaybeEq)
 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)
@@ -100,7 +102,7 @@ lemma-fmap-denumerate-enumerate : {S : Set} {C : Set → S → Set} → (ShapeT
 lemma-fmap-denumerate-enumerate {S} {C} ShapeT {s = s} c = begin
   fmap (denumerate ShapeT c) (fill s (allFin (arity s)))
     ≡⟨ fill-fmap (denumerate ShapeT c) s (allFin (arity s)) ⟩
-  fill s (map (flip lookupVec (content c)) (allFin (arity s)))
+  fill s (map (lookupVec (content c)) (allFin (arity s)))
     ≡⟨ P.cong (fill s) (map-lookup-allFin (content c)) ⟩
   fill s (content c)
     ≡⟨ content-fill c ⟩
@@ -275,7 +277,7 @@ module _ (G : Get) where
     contentV (fmapV (flip lookupM (h↦h′ h)) (get t))
       ≡⟨ Shaped.fmap-content ViewShapeT (flip lookupM (h↦h′ h)) (get t) ⟩
     map (flip lookupM (h↦h′ h)) (contentV (get t))
-      ≡⟨ lemma-exchange-maps (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
+      ≡⟨ lemma-exchange-maps (h↦h′ h) h (lemma-union-not-used h (reshape g′ (arityS (gl₁ j)))) (lemma-assoc-domain (contentV (get t)) (contentV v) ph) ⟩
     map (flip lookupM h) (contentV (get t))
       ≈⟨ lemma-2 (contentV (get t)) (contentV v) h ph ⟩
     map just (contentV v)