Link TODOs to PRs in agda-sets

Author: facundominguez

src/Ledger/Conway/Conformance/Equivalence/Map.agda

@@ -614,6 +614,8 @@ module _  {A B : Type}
       filterᵐ-singleton-true p .proj₁ = proj₂ ∘ (from ∈-filter)
       filterᵐ-singleton-true {k}{v} p .proj₂ {a} x = to ∈-filter (subst P′ (sym (from ∈-singleton x)) p , x)
 
+      -- TODO: move to agda-sets
+      -- https://github.com/input-output-hk/agda-sets/pull/19
       filterᵐ-singleton-false : ¬ P k → filterᵐ P′ ❴ k , v ❵ ≡ᵐ ∅
       filterᵐ-singleton-false ¬p .proj₁ x =
         ⊥-elim $ ¬p $ subst P′ (from ∈-singleton $ proj₂ (from ∈-filter x)) (proj₁ $ from ∈-filter x)
@@ -656,6 +658,8 @@ module _  {A B : Type}
       lem-add-excluded p =
         filterᵐ-∪⁺-distr _ _ ⟨≈⟩ ∪⁺-cong-l (filterᵐ-singleton-false p) ⟨≈⟩ ∪⁺-id-r _
 
+      -- TODO: move to agda-sets
+      -- https://github.com/input-output-hk/agda-sets/pull/19
       lem-add-excluded-∪ˡ
         : (m : A ⇀ B)
         → ¬ P k

src/Ledger/Conway/Specification/Ledger/Properties/Base.lagda.md

@@ -114,6 +114,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
     dpMap-rmOrphanDRepVotes certState govSt = sym (fmap-∘ govSt) -- map proj₁ ∘ map (map₂ _) ≡ map (proj₁ ∘ map₂ _) ≡ map proj₁
 
 -- TODO: Move these proofs to agda-sets
+-- https://github.com/input-output-hk/agda-sets/pull/18
 module _ {A V : Set} ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄ ⦃ dA : DecEq A ⦄ {m m' : A ⇀ V} where
   open import Function.Reasoning
 

src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md

@@ -141,6 +141,8 @@ module _ -- ASSUMPTION --
       disjoint-sing dp∉d a∈d a∈sing
         rewrite from ∈-dom-singleton-pair a∈sing = dp∉d a∈d
 
+      -- TODO: remove after adopting
+      -- https://github.com/input-output-hk/agda-sets/pull/17
       indexedSumᵐ-∪ˡ-∪ˡᶠ
         : ∀ m m'
         → indexedSumᵐ proj₂ ((m ∪ˡ m') ᶠᵐ) ≡ indexedSumᵐ proj₂ ((m ᶠᵐ) ∪ˡᶠ (m' ᶠᵐ))