final hole filled!

...thanks @WhatisRT! :)
IntersectMBO · Jul 12, 2023 · 154fcaf · 154fcaf
1 parent ecb4313
commit 154fcaf
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 17 deletions.
diff --git a/src/Axiom/Set/TotalMapOn.agda b/src/Axiom/Set/TotalMapOn.agda
@@ -120,8 +120,11 @@ module _ {X : Set A} where
   FunOn⇒TotalMapOn ∈-uip  _  .left-unique-rel    = left-unique-mapOn X ∈-uip
   FunOn⇒TotalMapOn _      f  .total-rel {a} a∈X  = to ∈-map ((a , f (a , a∈X)) , refl , (∈-map′ ∈-DSet))
 
-  -- It would be nice to have this general identity, but I don't know how to prove it yet.
-  -- lookup∘FunOn⇒TotalMapOn-id  : (∈-uip : ∈-irrelevant X){f : Σ A (_∈ X) → B}{aa : Σ A (_∈ X)}
-  --                             → lookup (FunOn⇒TotalMapOn ∈-uip f) aa ≡ f aa
-  -- lookup∘FunOn⇒TotalMapOn-id = {!!}
+  FunOn∈TotalMapOn  : (∈-uip : ∈-irrelevant X){f : Σ A (_∈ X) → B}{aa : Σ A (_∈ X)}
+                    → (proj₁ aa , f aa) ∈ rel (FunOn⇒TotalMapOn ∈-uip f)
+  FunOn∈TotalMapOn _ = ∈-map′ ∈-DSet
+
+  lookup∘FunOn⇒TotalMapOn-id  : (∈-uip : ∈-irrelevant X){f : Σ A (_∈ X) → B}{aa : Σ A (_∈ X)}
+                              → lookup (FunOn⇒TotalMapOn ∈-uip f) aa ≡ f aa
+  lookup∘FunOn⇒TotalMapOn-id ∈-uip {f} {a , a∈X} = ∈-rel→lookup-≡ ((FunOn⇒TotalMapOn ∈-uip f)) (FunOn∈TotalMapOn ∈-uip)
 
diff --git a/src/Ledger/TokenAlgebra/ValueSet.lagda b/src/Ledger/TokenAlgebra/ValueSet.lagda
@@ -98,23 +98,11 @@ module _ {X : ℙ AssetId} {∈-uip : ∈-irrelevant X} where
     g = lookup v
     f+g aa = f aa + g aa
 
-  lookup∘FunOn⇒TotalMapOn-id  : {f : Σ AssetId (_∈ X) → Quantity}{aa : Σ AssetId (_∈ X)}
-                              → lookup (FunOn⇒TotalMapOn ∈-uip f) aa ≡ f aa
-  lookup∘FunOn⇒TotalMapOn-id {f} {a , a∈X} = begin
-    lookup (FunOn⇒TotalMapOn ∈-uip f) (a , a∈X)                                                                         ≡⟨ ≡.refl ⟩
-    proj₁ (to dom∈ ((total-rel (FunOn⇒TotalMapOn ∈-uip f)) {a} a∈X))                                                    ≡⟨ ≡.refl ⟩
-    proj₁ (to dom∈ (to ∈-map ((a , f (a , a∈X)) , ≡.refl , (∈-map′{f = (λ x → proj₁ x , f x)} (∈-DSet{a = a}{a∈X})))))  ≡⟨ ≡.refl ⟩
-    proj₁ (to dom∈ (∈-map′ (∈-map′{f = (λ x → proj₁ x , f x)} (∈-DSet{a = a}{a∈X}))))                                   ≡⟨ {!!} ⟩
-    proj₁ ((f (a , a∈X)) , ((a , f (a , a∈X)) ∈ rel (FunOn⇒TotalMapOn ∈-uip f)))                                        ≡⟨ ≡.refl ⟩
-    f (a , a∈X)                                                                                                         ∎
-  -- Motice all the refls, which make it clear that I haven't really made progress toward the proof.
-  -- (It's the last proof remaining for this token algebra example... please help fill it!)
-
   ⊕-lemma : (u v : X ⇒ Quantity) → (aa : Σ AssetId (_∈ X))
    →       lookup (u ⊕ v) aa ≡ lookup u aa + lookup v aa
   ⊕-lemma u v (a , a∈X) = begin
     lookup (u ⊕ v) (a , a∈X) ≡⟨ ≡.refl ⟩
-    lookup (FunOn⇒TotalMapOn ∈-uip (λ x → lookup u x + lookup v x)) (a , a∈X) ≡⟨ lookup∘FunOn⇒TotalMapOn-id ⟩
+    lookup (FunOn⇒TotalMapOn ∈-uip (λ x → lookup u x + lookup v x)) (a , a∈X) ≡⟨ lookup∘FunOn⇒TotalMapOn-id ∈-uip ⟩
     lookup u (a , a∈X) + lookup v (a , a∈X) ∎