fix compilation with agda 2.5.1, agda-stdlib 0.12

1 files changed, 2 insertions, 2 deletions

diff --git a/Bidir.agda b/Bidir.agda
index 790f9b9..1022fab 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -144,7 +144,7 @@ theorem-1 G {i} s = begin
           h′↦r = (λ f′ → fmapS f′ t) ∘ flip lookupM
 
 
-lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
+lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → (f <$> ma) ≡ just b → ∃ λ a → ma ≡ just a
 lemma-<$>-just (just x) f<$>ma≡just-b = x , refl
 lemma-<$>-just nothing  ()
 
@@ -218,7 +218,7 @@ module _ (G : Get) where
   open Shaped SourceShapeT using () renaming (sequence to sequenceSource)
   open Shaped ViewShapeT using () renaming (sequence to sequenceView)
 
-  lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → get <$> sequenceSource v ≡ sequenceView (get v)
+  lemma-get-sequence : {A : Set} → {i : I} {v : SourceContainer (Maybe A) (gl₁ i)} {r : SourceContainer A (gl₁ i)} → sequenceSource v ≡ just r → (get <$> sequenceSource v) ≡ sequenceView (get v)
   lemma-get-sequence {v = v} {r = r} p = begin
     get <$> sequenceSource v
       ≡⟨ cong (_<$>_ get ∘ sequenceSource) (lemma-sequence-successful SourceShapeT v p) ⟩