From ce4ea63db5e11b150058894f98b4a36a3003c95a Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 23 Apr 2024 17:45:31 -0500
Subject: Add merge and unmerge properties

---
 FinMerge.agda | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'FinMerge.agda')

diff --git a/FinMerge.agda b/FinMerge.agda
index c75e982..d7b3f0b 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -11,7 +11,7 @@ open import Data.Product using (_×_; _,_; Σ-syntax; map₂; proj₁; proj₂)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
 open import Relation.Binary.PropositionalEquality.Properties using (module ≡-Reasoning)
 open import Function using (id ; _∘_ ; _$_)
-open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
+open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe; map)
 
 open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
 
@@ -25,7 +25,7 @@ pluck : m ≤ n → Fin (ℕ.suc n) → Maybe (Fin n)
 pluck z≤n Fin.zero = nothing
 pluck z≤n (Fin.suc x) = just x
 pluck (s≤s m) Fin.zero = just Fin.zero
-pluck (s≤s m) (Fin.suc x) = Data.Maybe.Base.map Fin.suc (pluck m x)
+pluck (s≤s m) (Fin.suc x) = map Fin.suc (pluck m x)
 
 -- Send nothing to the specified m
 unpluck : m ≤ n → Maybe (Fin n) → Fin (ℕ.suc n)
@@ -39,7 +39,7 @@ unpluck (s≤s m) (just (Fin.suc x)) = Fin.suc (unpluck m (just x))
 merge : {i j : ℕ} → i < j ≤ n → Fin (ℕ.suc n) → Fin n
 merge (lt , le) x = fromMaybe (fromℕ< (≤-trans lt le)) (pluck le x)
 
--- Merge two elements of a finite set
+-- Left-adjoint to merge
 unmerge : {i j : ℕ} → i < j ≤ n → Fin n → Fin (ℕ.suc n)
 unmerge (lt , le) x = unpluck le (just x)
 
@@ -48,6 +48,7 @@ glue-once {n} (less (i<j , s≤s j≤n)) = n , merge (i<j , j≤n)
 glue-once {n} (equal i≡j) = ℕ.suc n , id
 glue-once {n} (greater (j<i , s≤s i≤n)) = n , merge (j<i , i≤n)
 
+-- Merge and unmerge
 glue-unglue-once
     : {i j : Fin (ℕ.suc n)}
     → Ordering i j
-- 
cgit v1.2.3