From 54c29d2ce4d4e8a33d77bc787b2c5132f2089835 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Mon, 24 Feb 2014 14:58:01 +0100 Subject: theorem-2 works with EqR rather than SetoidReasoning again --- Bidir.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 832f172..43d8580 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -215,7 +215,7 @@ sequence-cong {S} (VecEq._∷-cong_ nothin theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v theorem-2 G j s v u p with (lemma->>=-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p) theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′) -theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ +theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin get <$> (just u) ≡⟨ cong (_<$>_ get) (sym p) ⟩ get <$> (bff G j s v) @@ -233,7 +233,7 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid sequenceV (map just v) ≡⟨ lemma-just-sequence v ⟩ just v ∎) - where open SetoidReasoning + where open EqR (MaybeSetoid (VecISetoid A.setoid at _)) open Get G s′ = enumerate s g = fromFunc (denumerate s) -- cgit v1.2.3