summaryrefslogtreecommitdiff
path: root/Bidir.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Bidir.agda')
-rw-r--r--Bidir.agda8
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)