From 09d2125aeaacdee48eadd72401e0e63a1c0a85bd Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 14 Jul 2023 22:45:17 -0700
Subject: [PATCH] Add note to self

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 NatMap.agda | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/NatMap.agda b/NatMap.agda
index 9349210..0df05ba 100644
--- a/NatMap.agda
+++ b/NatMap.agda
@@ -46,3 +46,11 @@ merge f m₁@(x₁@(n₁ , a₁) ∷ xs₁) m₂@(x₂@(n₂ , a₂) ∷ xs₂)
 
 testMerge : merge (_++_) ((1 , "one") ∷ (2 , "two") ∷ []) ((2 , "two") ∷ (3 , "three") ∷ []) ≡ (1 , "one") ∷ (2 , "twotwo") ∷ (3 , "three") ∷ []
 testMerge = refl
+
+-- Note to self: will it be tricky to define a Semilattice instance for this?
+--               I'm worried because proofs will likely require knowing the ordering -- merge certainly relies on it, but
+--               we can't prove commutativity if the NatMap type includes a proof of ordering, because then we'll need
+--               to compare `<=` for equality, which are going to be defined in terms of `=`...
+--
+--               We might need to generalize Lattice and friends to use ≈. But then,
+--               pain in the ass for products because they'll need to lift ≈ ...