diff options
| author | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 21:47:21 +0200 |
|---|---|---|
| committer | Helmut Grohne <helmut@subdivi.de> | 2019-03-31 21:47:21 +0200 |
| commit | 121094635514bf07bb91d6b7d16a45674c74f34e (patch) | |
| tree | c7f9c952c05774fd78d9c25e615b0a4da26d6846 /Bidir.agda | |
| parent | 50f61bef184194fc48dd1415800830d032495f51 (diff) | |
| download | bidiragda-121094635514bf07bb91d6b7d16a45674c74f34e.tar.gz | |
FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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) |