diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 14:58:01 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2014-02-24 14:58:01 +0100 |
| commit | 54c29d2ce4d4e8a33d77bc787b2c5132f2089835 (patch) | |
| tree | 2720ad09a13963676ff6857c433b5768c97c1418 /Bidir.agda | |
| parent | 6958d1c19cda39564508e0638648eacf32c71509 (diff) | |
| download | bidiragda-54c29d2ce4d4e8a33d77bc787b2c5132f2089835.tar.gz | |
theorem-2 works with EqR rather than SetoidReasoning again
Diffstat (limited to 'Bidir.agda')
| -rw-r--r-- | Bidir.agda | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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) |