diff options
| -rw-r--r-- | Bidir.agda | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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) ⟩ |