wip proof

src/Ledger/Utxo/Properties.lagda

@@ -164,15 +164,64 @@ opaque
     where open MonoidMorphisms.IsMonoidHomomorphism
 
   helper : (f : TxOut → TxOutʰ) → disjoint (dom utxo) (dom utxo') → disjoint (dom (mapValues f utxo)) (dom (mapValues f utxo'))
-  helper = {!!}
+  helper {utxo} {utxo'} f x x₁ x₂ = x (dom-mapʳ⊆ x₁) (dom-mapʳ⊆ x₂)
 
   import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
-  -- map-⊆
+
+
+  -- ∈-∪ : ∀ {a} → (a ∈ X ⊎ a ∈ Y) ⇔ a ∈ X ∪ Y
+  -- ∈-∪ = proj₂ binary-unions
+  --
+  -- Goal: a ∈ (mapˢ f X ∪ mapˢ f Y)
+  -- x   : a ∈ (mapˢ f (X ∪ Y)) → a
+  --
+  -- Goal: a ∈ (mapˢ f (X ∪ Y))
+  -- x   : a ∈ (mapˢ f X ∪ mapˢ f Y)
+  --
+  -- q ∈
+  --  (X ∪ Y) = (X ∪ Y)
+
+-- Left hand side
+-- (f x) ∈ (mapˢ f (X ∪ Y))
+-- x ∈ X ∪ Y
+-- isLeft -- x ∈ X
+-- isRight -- x ∈ Y
+-- cong f x ∈ map f X
+-- ∪-⊆ˡ : X ⊆ X ∪ Y
+-- cong f x ∈ map f Y
+-- ∪-⊆ʳ : Y ⊆ X ∪ Y
+
+-- ∪-⊆ˡ : X ⊆ X ∪ Y
+-- ∪-⊆ʳ : Y ⊆ X ∪ Y
+-- Right Hand Side
+-- f x ∈ (mapˢ f X ∪ mapˢ f Y)
+-- f x ∈ mapˢ f X
+-- cong f x ∈ mapˢ f X
+-- x ∈ F X
+-- ∪-⊆ˡ : X ⊆ X ∪ Y
+-- x ∈ X ∪ Y
+-- cong f x ∈ mapˢ f (X ∪ Y)
+-- f x ∈ mapˢ f Y
+-- this is the same
+--
+
   mapUnion : ∀ {A B : Set}{X Y} → (f : A → B) → mapˢ f (X ∪ Y) ≡ᵉ mapˢ f X ∪ mapˢ f Y
-  mapUnion f = {!!}
+  mapUnion {A} {B} {X} {Y} f = {!!} , (λ x → {!!})
+
+
+{-
+  mapUnion : ∀ {A B : Set}{X Y} → (f : A → B) → mapˢ f (X ∪ Y) ≡ᵉ mapˢ f X ∪ mapˢ f Y
+  mapUnion {A} {B} {X} {Y} f =  begin
+    mapˢ f (X ∪ Y)
+    ≈⟨ {!∪-cong ? ?!} ⟩
+    mapˢ f X ∪ mapˢ f Y
+    ∎
+   where open SetoidReasoning ≡ᵉ-Setoid
+-}
+
 
-  helper' : (f : TxOut → TxOutʰ) → disjoint (dom utxo) (dom utxo') → proj₁ (mapValues f (utxo ∪ˡ utxo')) ≡ᵉ proj₁ (mapValues f utxo ∪ˡ mapValues f utxo')
+  helper' : (f : TxOut → TxOutʰ) → disjoint (dom utxo) (dom utxo') → (mapValues f (utxo ∪ˡ utxo')) ˢ ≡ᵉ (mapValues f utxo ∪ˡ mapValues f utxo') ˢ
   helper' {utxo = utxo} {utxo'} f x = begin
     proj₁ (mapValues f (utxo ∪ˡ utxo'))
     ≈⟨ map-≡ᵉ (disjoint-∪ˡ-∪ x) ⟩