From 121094635514bf07bb91d6b7d16a45674c74f34e Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 31 Mar 2019 21:47:21 +0200
Subject: FinMap.lemma-lookupM-fromFunc is almost
 Data.Vec.Properties.lookup∘tabulate
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Bidir.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index cbe693c..5587d20 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -130,7 +130,7 @@ theorem-1 G {i} s = begin
       h′↦r (fromFunc f)
         ≡⟨ P.refl ⟩
       fmapS (flip lookupM (fromFunc f)) t
-        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc f) t ⟩
+        ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lookup∘tabulate (just ∘ f)) t ⟩
       fmapS (Maybe.just ∘ f) t
         ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just f t ⟩
       fmapS just (fmapS f t)
-- 
cgit v1.2.3