Require bottom element to actually be bottom; finish proof

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Forward.agda

@@ -21,7 +21,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using () renaming (isLattice to isLatticeˡ)
 
 module WithProg (prog : Program) where
-    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
     open import Analysis.Forward.Evaluation L prog
     open Program prog
 
@@ -66,7 +66,7 @@ module WithProg (prog : Program) where
                            (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
 
         -- The fixed point of the 'analyze' function is our final goal.
-        open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+        open import Fixedpoint analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
             renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
             public

Equivalence.agda

@@ -2,7 +2,7 @@ module Equivalence where
 
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 
 module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
     IsReflexive : Set a
@@ -19,3 +19,10 @@ module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
             ≈-refl : IsReflexive
             ≈-sym : IsSymmetric
             ≈-trans : IsTransitive
+
+isEquivalence-≡ : ∀ {a} {A : Set a} → IsEquivalence A _≡_
+isEquivalence-≡ = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }

Fixedpoint.agda

@@ -5,8 +5,8 @@ module Fixedpoint {a} {A : Set a}
                   {h : ℕ}
                   {_≈_ : A → A → Set a}
                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
-                  (≈-Decidable : IsDecidable _≈_)
-                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  {{ ≈-Decidable : IsDecidable _≈_ }}
+                  {{flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_}}
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                           (IsFiniteHeightLattice._≼_ flA) f) where
@@ -28,24 +28,9 @@ private
         using ()
         renaming
             ( ⊥ to ⊥ᴬ
-            ; longestChain to longestChainᴬ
             ; bounded to boundedᴬ
             )
 
-
-    ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
-    ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
-    ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
-    ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
-    ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
-                    where
-                        ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
-                        ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
-
-                        x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
-                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
-
     -- using 'g', for gas, here helps make sure the function terminates.
     -- since A forms a fixed-height lattice, we must find a solution after
     -- 'h' steps at most. Gas is set up such that as soon as it runs
@@ -65,7 +50,7 @@ private
                     c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))
 
     fix : Σ A (λ a → a ≈ f a)
-    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))
 
 aᶠ : A
 aᶠ = proj₁ fix
@@ -85,4 +70,4 @@ private
     ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
 
 aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
-aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))

Isomorphism.agda

@@ -68,6 +68,7 @@ module TransportFiniteHeight
         renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
 
     instance
+        fixedHeight : IsLattice.FixedHeight lB height
         fixedHeight = record
             { ⊥ = f ⊥₁
             ; ⊤ = f ⊤₁

Language/Graphs.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl;
 open import Relation.Nullary using (¬_)
 
 open import Lattice
-open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct; fins; fins-complete)
 
 record Graph : Set where
     constructor MkGraph
@@ -124,28 +124,6 @@ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
-private
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    finValues 0 = ([] , Utils.empty)
-    finValues (suc n') =
-        let
-            (inds' , unids') = finValues n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
-    finValues-complete (suc n') zero = RelAny.here refl
-    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
-
 module _ (g : Graph) where
     open import Data.Product.Properties as ProdProp using ()
     private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
@@ -154,13 +132,13 @@ module _ (g : Graph) where
     open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
-    indices = proj₁ (finValues (Graph.size g))
+    indices = proj₁ (fins (Graph.size g))
 
     indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
-    indices-complete = finValues-complete (Graph.size g)
+    indices-complete = fins-complete (Graph.size g)
 
     indices-Unique : Unique indices
-    indices-Unique = proj₂ (finValues (Graph.size g))
+    indices-Unique = proj₂ (fins (Graph.size g))
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Lattice.agda

@@ -4,7 +4,8 @@ open import Equivalence
 import Chain
 
 open import Relation.Binary.Core using (_Preserves_⟶_ )
-open import Relation.Nullary using (Dec; ¬_)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Product using (_×_; Σ; _,_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
@@ -95,6 +96,12 @@ record IsSemilattice {a} (A : Set a)
                     (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                 ∎
 
+    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
+    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)
+
+    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
+    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -112,6 +119,18 @@ record IsSemilattice {a} (A : Set a)
             a₃
         ∎
 
+    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
+    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
+        begin
+            a₁
+        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
+            a₂ ⊔ a₁
+        ∼⟨ ⊔-comm _ _ ⟩
+            a₁ ⊔ a₂
+        ∼⟨ a₁⊔a₂≈a₂ ⟩
+            a₂
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -236,6 +255,37 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    private
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    open MyChain.Height fixedHeight using (⊥; ⊤) public
+
+    Known-⊥ : Set a
+    Known-⊥ = ∀ (a : A) → ⊥ ≼ a
+
+    Known-⊤ : Set a
+    Known-⊤ = ∀ (a : A) → a ≼ ⊤
+
+    -- If the equality is decidable, we can prove that the top and bottom
+    -- elements of the chain are least and greatest elements of the lattice
+    module _ {{≈-Decidable : IsDecidable _≈_}} where
+        open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
+
+        open MyChain.Height fixedHeight using (bounded; longestChain)
+
+        ⊥≼ : Known-⊥
+        ⊥≼ a with ≈-dec a ⊥
+        ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
+        ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)
+        ...         | yes ⊥≈a⊓⊥ = ≈-trans (⊔-comm ⊥ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥≈a⊓⊥) (absorb-⊔-⊓ a ⊥))
+        ...         | no ⊥ᴬ̷≈a⊓⊥ = ⊥-elim (MyChain.Bounded-suc-n bounded (MyChain.step x≺⊥ ≈-refl longestChain))
+                        where
+                            ⊥⊓a̷≈⊥ : ¬ (⊥ ⊓ a) ≈ ⊥
+                            ⊥⊓a̷≈⊥ = λ ⊥⊓a≈⊥ → ⊥ᴬ̷≈a⊓⊥ (≈-trans (≈-sym ⊥⊓a≈⊥) (⊓-comm _ _))
+
+                            x≺⊥ : (⊥ ⊓ a) ≺ ⊥
+                            x≺⊥ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ ⊔ (⊥ ⊓ a)}) (absorb-⊔-⊓ ⊥ a)) , ⊥⊓a̷≈⊥)
+
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}

Lattice/Builder.agda

@@ -0,0 +1,885 @@
+module Lattice.Builder where
+
+open import Lattice
+open import Equivalence
+open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬; ∈-cartesianProduct; foldr₁; x∷xs≢[])
+open import Data.Nat as Nat using (ℕ)
+open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
+open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
+open import Data.Maybe.Properties using (just-injective)
+open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
+open import Data.List.Membership.Propositional as MemProp using (lose) renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
+open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺; ∈-filter⁻ to ∈ˡ-filter⁻; ∈-filter⁺ to ∈ˡ-filter⁺; ∈-lookup to ∈ˡ-lookup)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?; satisfied; index)
+open import Data.List.Relation.Unary.Any.Properties using (¬Any[]; lookup-result)
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; universal; all?)
+open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
+open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr; filter) renaming (_++_ to _++ˡ_)
+open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂; uncurry)
+open import Data.Empty using (⊥-elim)
+open import Relation.Nullary using (¬_; Dec; yes; no; ¬?; _×-dec_)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Relation.Binary using () renaming (Decidable to Decidable²)
+open import Relation.Unary using (Decidable)
+open import Relation.Unary.Properties using (_∩?_)
+open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
+
+record Graph : Set where
+    constructor mkGraph
+    field
+        size : ℕ
+
+    Node : Set
+    Node = Fin (Nat.suc size)
+
+    nodes = fins (Nat.suc size)
+
+    nodes-complete = fins-complete (Nat.suc size)
+
+    Edge : Set
+    Edge = Node × Node
+
+    field
+        edges : List Edge
+
+    nodes-nonempty : ¬ (proj₁ nodes ≡ [])
+    nodes-nonempty ()
+
+    data Path : Node → Node → Set where
+        done : ∀ {n : Node} → Path n n
+        step : ∀ {n₁ n₂ n₃ : Node} →  (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
+
+    data IsDone : ∀ {n₁ n₂} → Path n₁ n₂ → Set where
+        isDone : ∀ {n : Node} → IsDone (done {n})
+
+    IsDone? : ∀ {n₁ n₂} → Decidable (IsDone {n₁} {n₂})
+    IsDone? done = yes isDone
+    IsDone? (step _ _) = no (λ {()})
+
+    _++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
+    done ++ p = p
+    (step e p₁) ++ p₂ = step e (p₁ ++ p₂)
+
+    ++-done : ∀ {n₁ n₂} (p : Path n₁ n₂) → p ++ done ≡ p
+    ++-done done = refl
+    ++-done (step e∈edges p) rewrite ++-done p = refl
+
+    ++-assoc : ∀ {n₁ n₂ n₃ n₄} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) (p₃ : Path n₃ n₄) →
+                 (p₁ ++ p₂) ++ p₃ ≡ p₁ ++ (p₂ ++ p₃)
+    ++-assoc done p₂ p₃ = refl
+    ++-assoc (step n₁,n∈edges p₁) p₂ p₃ rewrite ++-assoc p₁ p₂ p₃ = refl
+
+    IsDone-++ˡ : ∀ {n₁ n₂ n₃} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) →
+                 ¬ IsDone p₁ → ¬ IsDone (p₁ ++ p₂)
+    IsDone-++ˡ done _ done≢done = ⊥-elim (done≢done isDone)
+
+    interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
+    interior done = []
+    interior (step _ done) = []
+    interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
+
+    interior-extend : ∀ {n₁ n₂ n₃} → (p : Path n₁ n₂) →  (n₂,n₃∈edges : (n₂ , n₃) ∈ˡ edges) →
+                      let p' = (p ++ (step n₂,n₃∈edges done))
+                      in (interior p' ≡ interior p) ⊎ (interior p' ≡ interior p ++ˡ (n₂ ∷ []))
+    interior-extend done _ = inj₁ refl
+    interior-extend (step n₁,n₂∈edges done) n₂n₃∈edges = inj₂ refl
+    interior-extend {n₂ = n₂} (step {n₂ = n} n₁,n∈edges p@(step _ _)) n₂n₃∈edges
+        with p ++ (step n₂n₃∈edges done) | interior-extend p n₂n₃∈edges
+    ...   | done | inj₁ []≡intp rewrite sym []≡intp = inj₁ refl
+    ...   | done | inj₂ []=intp++[n₂] with () ← ++ˡ-conicalʳ (interior p) (n₂ ∷ []) (sym []=intp++[n₂])
+    ...   | step _ p | inj₁ IH rewrite IH = inj₁ refl
+    ...   | step _ p | inj₂ IH rewrite IH = inj₂ refl
+
+    interior-++ : ∀ {n₁ n₂ n₃} → (p₁ : Path n₁ n₂) →  (p₂ : Path n₂ n₃) →
+                    ¬ IsDone p₁ → ¬ IsDone p₂ →
+                    interior (p₁ ++ p₂) ≡ interior p₁ ++ˡ (n₂ ∷ interior p₂)
+    interior-++ done _ done≢done _ = ⊥-elim (done≢done isDone)
+    interior-++ _ done _ done≢done = ⊥-elim (done≢done isDone)
+    interior-++ (step _ done) (step _ _) _ _ = refl
+    interior-++ (step n₁,n∈edges p@(step n,n'∈edges p')) p₂ _ p₂≢done
+        rewrite interior-++ p p₂ (λ {()}) p₂≢done = refl
+
+    SimpleWalkVia : List Node → Node → Node → Set
+    SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (_∈ˡ ns) (interior p))
+
+    SimpleWalk-extend : ∀ {n₁ n₂ n₃ ns} →  (w : SimpleWalkVia ns n₁ n₂) → (n₂ , n₃) ∈ˡ edges →  All (λ nʷ →  ¬ nʷ ≡ n₂) (interior (proj₁ w)) → n₂ ∈ˡ ns → SimpleWalkVia ns n₁ n₃
+    SimpleWalk-extend (p , (Unique-intp , intp⊆ns)) n₂,n₃∈edges w≢n₂ n₂∈ns
+        with p ++ (step n₂,n₃∈edges done) | interior-extend p n₂,n₃∈edges
+    ...   | p' | inj₁ intp'≡intp rewrite sym intp'≡intp = (p' , Unique-intp , intp⊆ns)
+    ...   | p' | inj₂ intp'≡intp++[n₂]
+            with intp++[n₂]⊆ns ←  ++ˡ⁺ intp⊆ns (n₂∈ns ∷ [])
+            rewrite sym intp'≡intp++[n₂] = (p' , (subst Unique (sym intp'≡intp++[n₂]) (Unique-append (¬Any-map sym (All¬-¬Any w≢n₂)) Unique-intp) , intp++[n₂]⊆ns))
+
+    ∈ˡ-narrow : ∀ {x y : Node} {ys : List Node} → x ∈ˡ (y ∷ ys) → ¬ y ≡ x → x ∈ˡ ys
+    ∈ˡ-narrow (here refl) x≢y = ⊥-elim (x≢y refl)
+    ∈ˡ-narrow (there x∈ys) _ = x∈ys
+
+    SplitSimpleWalkViaHelp : ∀ {n n₁ n₂ ns} (nⁱ : Node)
+                                            (w : SimpleWalkVia (n ∷ ns) n₁ n₂)
+                                            (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
+                                            ¬ IsDone p₁ → ¬ IsDone p₂ →
+                                            All (_∈ˡ ns) (interior p₁) →
+                                            proj₁ w ≡ p₁ ++ p₂ →
+                                            (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
+    SplitSimpleWalkViaHelp nⁱ w done _ done≢done _ _ _ = ⊥-elim (done≢done isDone)
+    SplitSimpleWalkViaHelp nⁱ w p₁ done _ done≢done _ _ = ⊥-elim (done≢done isDone)
+    SplitSimpleWalkViaHelp {n} {ns = ns} nⁱ w@(p , (Unique-intp , intp⊆ns)) p₁@(step _ _) p₂@(step {n₂ = nⁱ'} nⁱ,nⁱ',∈edges p₂') p₁≢done p₂≢done intp₁⊆ns p≡p₁++p₂
+        with intp≡intp₁++[n]++intp₂ ← trans (cong interior p≡p₁++p₂) (interior-++ p₁ p₂ p₁≢done p₂≢done)
+        with nⁱ∈n∷ns ∷ intp₂⊆n∷ns ← ++ˡ⁻ʳ (interior p₁) (subst (All (_∈ˡ (n ∷ ns))) intp≡intp₁++[n]++intp₂ intp⊆ns)
+        with nⁱ ≟ n
+    ...   | yes refl
+            with Unique-intp₁ ← Unique-++⁻ˡ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
+            with (push n≢intp₂ Unique-intp₂) ← Unique-++⁻ʳ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
+            = inj₁ (((p₁ , (Unique-intp₁ , intp₁⊆ns)) , (p₂ , (Unique-intp₂ , zipWith (uncurry ∈ˡ-narrow) (intp₂⊆n∷ns , n≢intp₂)))) , sym p≡p₁++p₂)
+    ...   | no nⁱ≢n
+            with p₂'
+    ...       | done
+                = let
+                      -- note: copied with below branch. can't use with <- to
+                      --       share and re-use because the termination checker loses the thread.
+                      p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
+                      n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
+                      intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
+                      intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
+                      intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
+                      -- end shared with below branch.
+                      Unique-intp₁++[nⁱ] = Unique-++⁻ˡ (interior p₁ ++ˡ (nⁱ ∷ [])) (subst Unique (trans intp≡intp₁++[n]++intp₂ (sym (++ˡ-assoc (interior p₁) (nⁱ ∷ []) []))) Unique-intp)
+                  in inj₂ ((p₁ ++ (step nⁱ,nⁱ',∈edges done) , (subst Unique (sym intp₁'=intp₁++[nⁱ]) Unique-intp₁++[nⁱ] , intp₁'⊆ns)) , sym p≡p₁++p₂)
+    ...       | p₂'@(step _ _)
+                = let p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
+                      n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
+                      intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
+                      intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
+                      intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
+                      p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ',∈edges done) p₂'))
+                  in SplitSimpleWalkViaHelp nⁱ' w p₁' p₂' (IsDone-++ˡ _ _ p₁≢done) (λ {()}) intp₁'⊆ns p≡p₁'++p₂'
+
+    SplitSimpleWalkVia : ∀ {n n₁ n₂ ns} (w : SimpleWalkVia (n ∷ ns) n₁ n₂) →  (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
+    SplitSimpleWalkVia (done , (_ , _)) = inj₂ ((done , (empty , [])) , refl)
+    SplitSimpleWalkVia (step n₁,n₂∈edges done , (_ , _)) = inj₂ ((step n₁,n₂∈edges done , (empty , [])) , refl)
+    SplitSimpleWalkVia w@(step {n₂ = nⁱ} n₁,nⁱ∈edges p@(step  _ _) , (push nⁱ≢intp Unique-intp , nⁱ∈ns ∷ intp⊆ns)) = SplitSimpleWalkViaHelp nⁱ w (step n₁,nⁱ∈edges done) p (λ {()}) (λ {()}) [] refl
+
+    open import Data.List.Membership.DecSetoid (decSetoid {A = Node} _≟_) using () renaming (_∈?_ to _∈ˡ?_)
+
+    splitFromInteriorʳ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
+                        Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ n ∷ interior p'))
+    splitFromInteriorʳ done ()
+    splitFromInteriorʳ (step _ done) ()
+    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , ([] , refl)))
+    splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
+        with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInteriorʳ p' n∈intp'
+        rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
+
+    splitFromInteriorˡ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
+                        Σ (Path n₁ n) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ interior p' ++ˡ ns))
+    splitFromInteriorˡ done ()
+    splitFromInteriorˡ (step _ done) ()
+    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (step n₁,n'∈edges done , ((λ {()}) , (interior p , refl)))
+    splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
+        with splitFromInteriorˡ p' n∈intp'
+    ...   | (p''@(step _ _) , (¬IsDone-p'' , (ns , intp'≡intp''++ns)))
+            rewrite intp'≡intp''++ns
+            = (step n₁,n'∈edges p'' , ((λ { () }) , (ns , refl)))
+    ...   | (done , (¬IsDone-Done , _)) = ⊥-elim (¬IsDone-Done isDone)
+
+    findCycleHelp : ∀ {n₁ nⁱ n₂} (p : Path n₁ n₂) (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
+                      ¬ IsDone p₁ → Unique (interior p₁) →
+                      p ≡ p₁ ++ p₂ →
+                      (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ IsDone (proj₁ w)))
+    findCycleHelp p p₁ done ¬IsDonep₁ Unique-intp₁ p≡p₁++done rewrite ++-done p₁ = inj₁ ((p₁ , (Unique-intp₁ , tabulate (λ {x} _ → nodes-complete x))) , sym p≡p₁++done)
+    findCycleHelp {nⁱ = nⁱ} p p₁ (step nⁱ,nⁱ'∈edges p₂') ¬IsDone-p₁ Unique-intp₁ p≡p₁++p₂
+        with nⁱ ∈ˡ? interior p₁
+    ...   | no nⁱ∉intp₁ =
+            let p₁' = p₁ ++ step nⁱ,nⁱ'∈edges done
+                intp₁'≡intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁ (λ {()}))
+                ¬IsDone-p₁' = IsDone-++ˡ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁
+                p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ'∈edges done) p₂'))
+                Unique-intp₁' = subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)
+            in findCycleHelp p p₁' p₂' ¬IsDone-p₁' Unique-intp₁' p≡p₁'++p₂'
+    ...   | yes nⁱ∈intp₁
+            with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInteriorʳ p₁ nⁱ∈intp₁
+            rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior pᶜ)) =
+            let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁
+            in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ (ns ++ˡ nⁱ ∷ [])  Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
+
+    findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) →  (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w →  ¬ IsDone (proj₁ w)))
+    findCycle done = inj₁ ((done , (empty , [])) , refl)
+    findCycle (step n₁,n₂∈edges done) = inj₁ ((step n₁,n₂∈edges done , (empty , [])) , refl)
+    findCycle p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) = findCycleHelp p (step n₁,n'∈edges done) p' (λ {()}) empty refl
+
+    toSimpleWalk : ∀ {n₁ n₂} (p : Path n₁ n₂) → SimpleWalkVia (proj₁ nodes) n₁ n₂
+    toSimpleWalk done = (done , (empty , []))
+    toSimpleWalk (step {n₂ = nⁱ} n₁,nⁱ∈edges p')
+        with toSimpleWalk p'
+    ...   | (done , _) = (step n₁,nⁱ∈edges done , (empty , []))
+    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
+            with nⁱ ∈ˡ? interior p''
+    ...       | no nⁱ∉intp'' = (step n₁,nⁱ∈edges p'' , (push (tabulate (λ { n∈intp'' refl →  nⁱ∉intp'' n∈intp'' })) Unique-intp'' , (nodes-complete nⁱ) ∷ intp''⊆nodes))
+    ...       | yes nⁱ∈intp''
+                with splitFromInteriorʳ p'' nⁱ∈intp''
+    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ⊥-elim (¬IsDone=p''ʳ isDone)
+    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) =
+                    -- no rewrites because then I can't reason about the return value of toSimpleWalk
+                    -- rewrite intp''≡ns++intp''ʳ
+                    -- rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ)) =
+                    let reassoc-intp''≡ns++intp''ʳ = subst (interior p'' ≡_) (sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ))) intp''≡ns++intp''ʳ
+                        intp''ʳ⊆nodes = ++ˡ⁻ʳ (ns ++ˡ nⁱ ∷ []) (subst (All (_∈ˡ (proj₁ nodes))) reassoc-intp''≡ns++intp''ʳ intp''⊆nodes)
+                        Unique-ns++intp''ʳ = subst Unique reassoc-intp''≡ns++intp''ʳ Unique-intp''
+                        nⁱ∈p''ˡ = ∈ˡ-++⁺ʳ ns {ys = nⁱ ∷ []} (here refl)
+                    in (step n₁,nⁱ∈edges p''ʳ , (Unique-narrow (ns ++ˡ nⁱ ∷ []) Unique-ns++intp''ʳ nⁱ∈p''ˡ , nodes-complete nⁱ ∷ intp''ʳ⊆nodes ))
+
+    toSimpleWalk-IsDone⁻ : ∀ {n₁ n₂} (p : Path n₁ n₂) →
+                          ¬ IsDone p → ¬ IsDone (proj₁ (toSimpleWalk p))
+    toSimpleWalk-IsDone⁻ done ¬IsDone-p _ = ¬IsDone-p isDone
+    toSimpleWalk-IsDone⁻ (step {n₂ = nⁱ} n₁,nⁱ∈edges p') _ isDone-w
+        with toSimpleWalk p'
+    ...   | (done , _) with () ← isDone-w
+    ...   | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
+            with nⁱ ∈ˡ? interior p''
+    ...       | no nⁱ∉intp'' with () ← isDone-w
+    ...       | yes nⁱ∈intp''
+                with splitFromInteriorʳ p'' nⁱ∈intp''
+    ...           | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ¬IsDone=p''ʳ isDone
+    ...           | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ)))
+                    with () ← isDone-w
+
+    Adjacency : Set
+    Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
+
+    Adjacency-update : ∀ (n₁ n₂ : Node) → (List (Path n₁ n₂) → List (Path n₁ n₂)) → Adjacency → Adjacency
+    Adjacency-update n₁ n₂ f adj n₁' n₂'
+        with n₁ ≟ n₁' | n₂ ≟ n₂'
+    ...  | yes refl | yes refl = f (adj n₁ n₂)
+    ...  | _        | _        = adj n₁' n₂'
+
+    Adjacency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
+    Adjacency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_)
+
+    Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjacency-append ps adj n₁' n₂'
+    Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj
+        with n₁ ≟ n₁' | n₂ ≟ n₂'
+    ...   | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj
+    ...   | yes refl | no _ = p∈adj
+    ...   | no _ | no _ = p∈adj
+    ...   | no _ | yes _ = p∈adj
+
+    adj⁰ : Adjacency
+    adj⁰ n₁ n₂
+        with n₁ ≟ n₂
+    ... | yes refl = done ∷ []
+    ... | no _ = []
+
+    adj⁰-done : ∀ n →  done ∈ˡ adj⁰ n n
+    adj⁰-done n
+        with n ≟ n
+    ... | yes refl = here refl
+    ... | no n≢n = ⊥-elim (n≢n refl)
+
+    seedWithEdges : ∀ (es : List Edge) →  (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → Adjacency
+    seedWithEdges es e∈es⇒e∈edges adj = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((step n₁n₂∈edges done) ∷_)) adj (mapWith∈ˡ es (λ {e} e∈es →  (e , e∈es⇒e∈edges e∈es)))
+
+    seedWithEdges-monotonic : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ {p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
+    seedWithEdges-monotonic {es = []} e∈es⇒e∈edges p∈adj = p∈adj
+    seedWithEdges-monotonic {es = (n₁ , n₂) ∷ es} e∈es⇒e∈edges p∈adj = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (seedWithEdges-monotonic (λ e∈es → e∈es⇒e∈edges (there e∈es)) p∈adj)
+
+    e∈seedWithEdges : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) →  (step (e∈es⇒e∈edges n₁n₂∈es) done) ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
+    e∈seedWithEdges {es = []} e∈es⇒e∈edges ()
+    e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
+        with n₁' ≟ n₁' | n₂' ≟ n₂'
+    ...   | yes refl | yes refl = here refl
+    ...   | no n₁'≢n₁' | _ = ⊥-elim (n₁'≢n₁' refl)
+    ...   | _ | no n₂'≢n₂' = ⊥-elim (n₂'≢n₂' refl)
+    e∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} {adj} e∈es⇒e∈edges (there n₁n₂∈es) = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
+
+    adj¹ : Adjacency
+    adj¹ = seedWithEdges edges (λ x → x) adj⁰
+
+    adj¹-adj⁰ : ∀ {n₁ n₂ p} → p ∈ˡ adj⁰ n₁ n₂ → p ∈ˡ adj¹ n₁ n₂
+    adj¹-adj⁰ p∈adj⁰ = seedWithEdges-monotonic (λ x → x) p∈adj⁰
+
+    edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) →  (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
+    edge∈adj¹ = e∈seedWithEdges (λ x → x)
+
+    through : Node → Adjacency → Adjacency
+    through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
+
+    through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
+    through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
+
+    through-++ : ∀ adj n {n₁ n₂} {p₁ : Path n₁ n} {p₂ : Path n n₂} → p₁ ∈ˡ adj n₁ n → p₂ ∈ˡ adj n n₂ → (p₁ ++ p₂) ∈ˡ through n adj n₁ n₂
+    through-++ adj n p₁∈adj p₂∈adj = ∈ˡ-++⁺ˡ (∈ˡ-cartesianProductWith⁺ _++_ p₁∈adj p₂∈adj)
+
+    throughAll : List Node → Adjacency
+    throughAll = foldr through adj¹
+
+    throughAll-adj₁ : ∀ {n₁ n₂ p} ns → p ∈ˡ adj¹ n₁ n₂ → p ∈ˡ throughAll ns n₁ n₂
+    throughAll-adj₁ [] p∈adj¹ = p∈adj¹
+    throughAll-adj₁ (n ∷ ns) p∈adj¹ = through-monotonic (throughAll ns) n (throughAll-adj₁ ns p∈adj¹)
+
+    paths-throughAll : ∀ {n₁ n₂ : Node} (ns : List Node) (w : SimpleWalkVia ns n₁ n₂) →  proj₁ w ∈ˡ throughAll ns n₁ n₂
+    paths-throughAll {n₁} [] (done , (_ , _)) = adj¹-adj⁰ (adj⁰-done n₁)
+    paths-throughAll {n₁} [] (step e∈edges done , (_ , _)) = edge∈adj¹ e∈edges
+    paths-throughAll {n₁} [] (step _ (step _ _) , (_ , (() ∷ _)))
+    paths-throughAll (n ∷ ns) w
+        with SplitSimpleWalkVia w
+    ...  | inj₁ ((w₁ , w₂) , w₁++w₂≡w) rewrite sym w₁++w₂≡w = through-++ (throughAll ns) n (paths-throughAll ns w₁) (paths-throughAll ns w₂)
+    ...  | inj₂ (w' , w'≡w) rewrite sym w'≡w = through-monotonic (throughAll ns) n (paths-throughAll ns w')
+
+    adj : Adjacency
+    adj = throughAll (proj₁ nodes)
+
+    PathExists : Node → Node → Set
+    PathExists n₁ n₂ = Path n₁ n₂
+
+    PathExists? : Decidable² PathExists
+    PathExists? n₁ n₂
+        with allSimplePathsNoted ← paths-throughAll {n₁ = n₁} {n₂ = n₂} (proj₁ nodes)
+        with adj n₁ n₂
+    ...   | [] = no (λ p →  let w = toSimpleWalk p in ¬Any[] (allSimplePathsNoted w))
+    ...   | (p ∷ ps) = yes p
+
+    NoCycles : Set
+    NoCycles = ∀ {n} (p : Path n n) →  IsDone p
+
+    NoCycles? : Dec NoCycles
+    NoCycles? with any? (λ n → any? (Decidable-¬ IsDone?) (adj n n)) (proj₁ nodes)
+    ... | yes existsCycle =
+          no (λ ∀p,IsDonep →  let (n , n,n-cycle) = satisfied existsCycle in
+                              let (p , ¬IsDone-p) = satisfied n,n-cycle in
+                              ¬IsDone-p (∀p,IsDonep p))
+    ... | no noCycles =
+          yes (λ { done →  isDone
+                 ; p@(step {n₁ = n} _ _) →
+                    let w = toSimpleWalk p in
+                    let ¬IsDone-w = toSimpleWalk-IsDone⁻ p (λ {()}) in
+                    let w∈adj = paths-throughAll (proj₁ nodes) w in
+                    ⊥-elim (noCycles (lose (nodes-complete n) (lose w∈adj ¬IsDone-w)))
+                 })
+
+    NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} →  p ∈ˡ adj n₁ n₂
+    NoCycles⇒adj-complete noCycles {n₁} {n₂} {p}
+        with findCycle p
+    ...   | inj₁ (w , w≡p) rewrite sym w≡p = paths-throughAll (proj₁ nodes) w
+    ...   | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (noCycles (proj₁ wᶜ)))
+
+    Is-⊤ : Node → Set
+    Is-⊤ n = All (PathExists n) (proj₁ nodes)
+
+    Is-⊥ : Node → Set
+    Is-⊥ n = All (λ n' → PathExists n' n) (proj₁ nodes)
+
+    Has-⊤ : Set
+    Has-⊤ = Any Is-⊤ (proj₁ nodes)
+
+    Has-⊤? : Dec Has-⊤
+    Has-⊤? = findUniversal (proj₁ nodes) PathExists?
+
+    Has-⊥ : Set
+    Has-⊥ = Any Is-⊥ (proj₁ nodes)
+
+    Has-⊥? : Dec Has-⊥
+    Has-⊥? = findUniversal (proj₁ nodes) (λ n₁ n₂ → PathExists? n₂ n₁)
+
+    Pred : Node → Node → Node → Set
+    Pred n₁ n₂ n = PathExists n n₁ × PathExists n n₂
+
+    Succ : Node → Node → Node → Set
+    Succ n₁ n₂ n = PathExists n₁ n × PathExists n₂ n
+
+    Pred? : ∀ (n₁ n₂ : Node) → Decidable (Pred n₁ n₂)
+    Pred? n₁ n₂ n = PathExists? n n₁ ×-dec PathExists? n n₂
+
+    Suc? : ∀ (n₁ n₂ : Node) → Decidable (Succ n₁ n₂)
+    Suc? n₁ n₂ n = PathExists? n₁ n ×-dec PathExists? n₂ n
+
+    preds : Node → Node → List Node
+    preds n₁ n₂ = filter (Pred? n₁ n₂) (proj₁ nodes)
+
+    sucs : Node → Node → List Node
+    sucs n₁ n₂ = filter (Suc? n₁ n₂) (proj₁ nodes)
+
+    Have-⊔ : Node → Node → Set
+    Have-⊔ n₁ n₂ = Σ Node (λ n →  Pred n₁ n₂ n × (∀ n' →  Pred n₁ n₂ n' → PathExists n' n))
+
+    Have-⊓ : Node → Node → Set
+    Have-⊓ n₁ n₂ = Σ Node (λ n →  Succ n₁ n₂ n × (∀ n' →  Succ n₁ n₂ n' → PathExists n n'))
+
+    -- when filtering nodes by a predicate P, then trying to find a universal
+    -- element according to another predicate Q, the universality can be
+    -- extended from "element of the filtered list for to which all other elements relate" to
+    -- "node satisfying P to which all other nodes satisfying P relate".
+    filter-nodes-universal : ∀ {P : Node → Set} (P? : Decidable P) -- e.g. Pred n₁ n₂
+                               {Q : Node → Node → Set} (Q? : Decidable² Q) -- e.g. PathExists? n' n
+                               → Dec (Σ Node λ n → P n × (∀ n' → P n' → Q n n'))
+    filter-nodes-universal {P = P} P? {Q = Q} Q?
+        with findUniversal (filter P? (proj₁ nodes)) Q?
+    ...   | yes founduni =
+            let idx = index founduni
+                n = Any.lookup founduni
+                n∈filter = ∈ˡ-lookup idx
+                (_ , Pn) = ∈ˡ-filter⁻ P? {xs = proj₁ nodes} n∈filter
+                nuni = lookup-result founduni
+            in yes (n , (Pn , λ n' Pn' →
+                                    let n'∈filter = ∈ˡ-filter⁺ P? (nodes-complete n') Pn'
+                                    in lookup nuni n'∈filter))
+    ...   | no nouni = no λ (n , (Pn , nuni')) →
+                           let n∈filter = ∈ˡ-filter⁺ P? (nodes-complete n) Pn
+                               nuni = tabulate {xs = filter P? (proj₁ nodes)} (λ {n'} n'∈filter →  nuni' n' (proj₂ (∈ˡ-filter⁻ P? {xs = proj₁ nodes} n'∈filter)))
+                           in nouni (lose n∈filter nuni)
+
+    Have-⊔? : Decidable² Have-⊔
+    Have-⊔? n₁ n₂ = filter-nodes-universal (Pred? n₁ n₂) (λ n₁ n₂ → PathExists? n₂ n₁)
+
+    Have-⊓? : Decidable² Have-⊓
+    Have-⊓? n₁ n₂ = filter-nodes-universal (Suc? n₁ n₂) PathExists?
+
+    Total-⊔ : Set
+    Total-⊔ = ∀ n₁ n₂ → Have-⊔ n₁ n₂
+
+    Total-⊓ : Set
+    Total-⊓ = ∀ n₁ n₂ → Have-⊓ n₁ n₂
+
+    P-Total? : ∀ {P : Node → Node → Set} (P? : Decidable² P) → Dec (∀ n₁ n₂ → P n₁ n₂)
+    P-Total? {P} P?
+        with all? (λ (n₁ , n₂) → P? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
+    ...   | yes allP = yes λ n₁ n₂ →
+            let n₁n₂∈prod = ∈-cartesianProduct (nodes-complete n₁) (nodes-complete n₂)
+            in lookup allP n₁n₂∈prod
+    ...   | no ¬allP = no λ allP → ¬allP (universal (λ (n₁ , n₂) → allP n₁ n₂) _)
+
+    Total-⊔? : Dec Total-⊔
+    Total-⊔? = P-Total? Have-⊔?
+
+    Total-⊓? : Dec Total-⊓
+    Total-⊓? = P-Total? Have-⊓?
+
+    module Basic (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
+        n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂
+        n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁
+            with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁)
+        ...   | done | done | _ = refl
+        ...   | step _ _ | done | _ = refl
+        ...   | done | step _ _ | _ = refl
+        ...   | step _ _ | step _ _ | ()
+
+        _⊔_ : Node → Node → Node
+        _⊔_ n₁ n₂ = proj₁ (total-⊔ n₁ n₂)
+
+        _⊓_ : Node → Node → Node
+        _⊓_ n₁ n₂ = proj₁ (total-⊓ n₁ n₂)
+
+        ⊤ : Node
+        ⊤ = foldr₁ nodes-nonempty _⊔_
+
+        ⊥ : Node
+        ⊥ = foldr₁ nodes-nonempty _⊓_
+
+        _≼_ : Node → Node → Set
+        _≼_ n₁ n₂ = n₁ ⊔ n₂ ≡ n₂
+
+        n₁≼n₂→PathExistsn₂n₁ : ∀ n₁ n₂ → (n₁ ≼ n₂) → PathExists n₂ n₁
+        n₁≼n₂→PathExistsn₂n₁ n₁ n₂ n₁⊔n₂≡n₂
+            with total-⊔ n₁ n₂ | n₁⊔n₂≡n₂
+        ...   | (_ , ((n₂→n₁ , _) , _)) | refl = n₂→n₁
+
+        PathExistsn₂n₁→n₁≼n₂ : ∀ n₁ n₂ → PathExists n₂ n₁ → (n₁ ≼ n₂)
+        PathExistsn₂n₁→n₁≼n₂ n₁ n₂ n₂→n₁
+            with total-⊔ n₁ n₂
+        ...   | (n , ((n→n₁ , n→n₂) , n'→n₁×n'→n₂⇒n'→n))
+                rewrite n₁→n₂×n₂→n₁⇒n₁≡n₂ n→n₂ (n'→n₁×n'→n₂⇒n'→n n₂ (n₂→n₁ , done)) = refl
+
+        foldr₁⊔-Pred : ∀ {ns : List Node} (ns≢[] : ¬ (ns ≡ [])) → let n = foldr₁ ns≢[] _⊔_ in All (PathExists n) ns
+        foldr₁⊔-Pred {ns = []} []≢[] = ⊥-elim ([]≢[] refl)
+        foldr₁⊔-Pred {ns = n₁ ∷ []} _ = done ∷ []
+        foldr₁⊔-Pred {ns = n₁ ∷ ns'@(n₂ ∷ ns'')} ns≢[] =
+            let
+                ns'≢[] = x∷xs≢[] n₂ ns''
+                n' = foldr₁ ns'≢[] _⊔_
+                (n , ((n→n₁ , n→n') , r)) = total-⊔ n₁ n'
+            in
+                n→n₁ ∷ map (n→n' ++_) (foldr₁⊔-Pred ns'≢[])
+
+        -- TODO: this is very similar structurally to foldr₁⊔-Pred
+        foldr₁⊓-Suc : ∀ {ns : List Node} (ns≢[] : ¬ (ns ≡ [])) → let n = foldr₁ ns≢[] _⊓_ in All (λ n' → PathExists n' n) ns
+        foldr₁⊓-Suc {ns = []} []≢[] = ⊥-elim ([]≢[] refl)
+        foldr₁⊓-Suc {ns = n₁ ∷ []} _ = done ∷ []
+        foldr₁⊓-Suc {ns = n₁ ∷ ns'@(n₂ ∷ ns'')} ns≢[] =
+            let
+                ns'≢[] = x∷xs≢[] n₂ ns''
+                n' = foldr₁ ns'≢[] _⊓_
+                (n , ((n₁→n , n'→n) , r)) = total-⊓ n₁ n'
+            in
+                n₁→n ∷ map (_++ n'→n) (foldr₁⊓-Suc ns'≢[])
+
+        ⊤-is-⊤ : Is-⊤ ⊤
+        ⊤-is-⊤ = foldr₁⊔-Pred nodes-nonempty
+
+        ⊥-is-⊥ : Is-⊥ ⊥
+        ⊥-is-⊥ = foldr₁⊓-Suc nodes-nonempty
+
+        ⊔-idemp : ∀ n → n ⊔ n ≡ n
+        ⊔-idemp n
+            with (n' , ((n'→n , _) , n''→n×n''→n⇒n''→n')) ← total-⊔ n n
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ n'→n (n''→n×n''→n⇒n''→n' n (done , done))
+
+        ⊓-idemp : ∀ n → n ⊓ n ≡ n
+        ⊓-idemp n
+            with (n' , ((n→n' , _) , n→n''×n→n''⇒n'→n'')) ← total-⊓ n n
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n→n''×n→n''⇒n'→n'' n (done , done)) n→n'
+
+        ⊔-comm : ∀ n₁ n₂ → n₁ ⊔ n₂ ≡ n₂ ⊔ n₁
+        ⊔-comm n₁ n₂
+            with (n₁₂ , ((n₁n₂→n₁ , n₁n₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₂₁ , ((n₂n₁→n₂ , n₂n₁→n₁) , n'→n₂×n'→n₁⇒n'→n₂₁)) ← total-⊔ n₂ n₁
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n'→n₂×n'→n₁⇒n'→n₂₁ n₁₂ (n₁n₂→n₂ , n₁n₂→n₁))
+                                (n'→n₁×n'→n₂⇒n'→n₁₂ n₂₁ (n₂n₁→n₁ , n₂n₁→n₂))
+
+        ⊓-comm : ∀ n₁ n₂ → n₁ ⊓ n₂ ≡ n₂ ⊓ n₁
+        ⊓-comm n₁ n₂
+            with (n₁₂ , ((n₁→n₁n₂ , n₂→n₁n₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+            with (n₂₁ , ((n₂→n₂n₁ , n₁→n₂n₁) , n₂→n'×n₁→n'⇒n₂₁→n')) ← total-⊓ n₂ n₁
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₂→n'⇒n₁₂→n' n₂₁ (n₁→n₂n₁ , n₂→n₂n₁))
+                                (n₂→n'×n₁→n'⇒n₂₁→n' n₁₂ (n₂→n₁n₂ , n₁→n₁n₂))
+
+        ⊔-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊔ n₂) ⊔ n₃ ≡ n₁ ⊔ (n₂ ⊔ n₃)
+        ⊔-assoc n₁ n₂ n₃
+            with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₁₂,₃ , ((n₁₂,₃→n₁₂ , n₁₂,₃→n₃) , n'→n₁₂×n'→n₃⇒n'→n₁₂,₃)) ← total-⊔ n₁₂ n₃
+            with (n₂₃ , ((n₂₃→n₂ , n₂₃→n₃) , n'→n₂×n'→n₃⇒n'→n₂₃)) ← total-⊔ n₂ n₃
+            with (n₁,₂₃ , ((n₁,₂₃→n₁ , n₁,₂₃→n₂₃) , n'→n₁×n'→n₂₃⇒n'→n₁,₂₃)) ← total-⊔ n₁ n₂₃
+            =
+                let n₁₂,₃→n₂₃ = n'→n₂×n'→n₃⇒n'→n₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₂ , n₁₂,₃→n₃)
+                    n₁₂,₃→n₁,₂₃ = n'→n₁×n'→n₂₃⇒n'→n₁,₂₃ n₁₂,₃ (n₁₂,₃→n₁₂ ++ n₁₂→n₁ , n₁₂,₃→n₂₃)
+                    n₁,₂₃→n₁₂ = n'→n₁×n'→n₂⇒n'→n₁₂ n₁,₂₃ (n₁,₂₃→n₁ , n₁,₂₃→n₂₃ ++ n₂₃→n₂)
+                    n₁,₂₃→n₁₂,₃ = n'→n₁₂×n'→n₃⇒n'→n₁₂,₃ n₁,₂₃ (n₁,₂₃→n₁₂ , n₁,₂₃→n₂₃ ++ n₂₃→n₃)
+                in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
+
+        ⊓-assoc : ∀ n₁ n₂ n₃ → (n₁ ⊓ n₂) ⊓ n₃ ≡ n₁ ⊓ (n₂ ⊓ n₃)
+        ⊓-assoc n₁ n₂ n₃
+          with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+          with (n₁₂,₃ , ((n₁₂→n₁₂,₃ , n₃→n₁₂,₃) , n₁₂→n'×n₃→n'⇒n₁₂,₃→n')) ← total-⊓ n₁₂ n₃
+          with (n₂₃ , ((n₂→n₂₃ , n₃→n₂₃) ,  n₂→n'×n₃→n'⇒n₂₃→n')) ← total-⊓ n₂ n₃
+          with (n₁,₂₃ , ((n₁→n₁,₂₃ , n₂₃→n₁,₂₃) ,  n₁→n'×n₂₃→n'⇒n₁,₂₃→n')) ← total-⊓ n₁ n₂₃
+          =
+            let n₁₂→n₁,₂₃ = n₁→n'×n₂→n'⇒n₁₂→n' n₁,₂₃ (n₁→n₁,₂₃ , n₂→n₂₃ ++ n₂₃→n₁,₂₃)
+                n₁₂,₃→n₁,₂₃ = n₁₂→n'×n₃→n'⇒n₁₂,₃→n' n₁,₂₃ (n₁₂→n₁,₂₃ , n₃→n₂₃ ++ n₂₃→n₁,₂₃)
+                n₂₃→n₁₂,₃ = n₂→n'×n₃→n'⇒n₂₃→n' n₁₂,₃ (n₂→n₁₂ ++ n₁₂→n₁₂,₃ , n₃→n₁₂,₃)
+                n₁,₂₃→n₁₂,₃ = n₁→n'×n₂₃→n'⇒n₁,₂₃→n' n₁₂,₃ (n₁→n₁₂ ++ n₁₂→n₁₂,₃ , n₂₃→n₁₂,₃)
+            in n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁₂,₃→n₁,₂₃ n₁,₂₃→n₁₂,₃
+
+        absorb-⊔-⊓ : ∀ n₁ n₂ → n₁ ⊔ (n₁ ⊓ n₂) ≡ n₁
+        absorb-⊔-⊓ n₁ n₂
+            with (n₁₂ , ((n₁→n₁₂ , n₂→n₁₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+            with (n₁,₁₂ , ((n₁,₁₂→n₁ , n₁,₁₂→n₁₂) , n'→n₁×n'→n₁₂⇒n'→n₁,₁₂)) ← total-⊔ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁,₁₂→n₁ (n'→n₁×n'→n₁₂⇒n'→n₁,₁₂ n₁ (done , n₁→n₁₂))
+
+        absorb-⊓-⊔ : ∀ n₁ n₂ → n₁ ⊓ (n₁ ⊔ n₂) ≡ n₁
+        absorb-⊓-⊔ n₁ n₂
+            with (n₁₂ , ((n₁₂→n₁ , n₁₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₁,₁₂ , ((n₁→n₁,₁₂ , n₁₂→n₁,₁₂) , n₁→n'×n₁₂→n'⇒n₁,₁₂→n')) ← total-⊓ n₁ n₁₂
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₁₂→n'⇒n₁,₁₂→n' n₁ (done , n₁₂→n₁)) n₁→n₁,₁₂
+
+        instance
+            isJoinSemilattice : IsSemilattice Node _≡_ _⊔_
+            isJoinSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊔-idemp
+                ; ⊔-comm = ⊔-comm
+                ; ⊔-assoc = ⊔-assoc
+                }
+
+            isMeetSemilattice : IsSemilattice Node _≡_ _⊓_
+            isMeetSemilattice = record
+                { ≈-equiv = isEquivalence-≡
+                ; ≈-⊔-cong = (λ { refl refl → refl })
+                ; ⊔-idemp = ⊓-idemp
+                ; ⊔-comm = ⊓-comm
+                ; ⊔-assoc = ⊓-assoc
+                }
+
+            isLattice : IsLattice Node _≡_ _⊔_ _⊓_
+            isLattice = record
+                { absorb-⊔-⊓ = absorb-⊔-⊓
+                ; absorb-⊓-⊔ = absorb-⊓-⊔
+                }
+
+    module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set λ L → Σ (FiniteHeightLattice L) λ fhl → FiniteHeightLattice.Known-⊥ fhl × FiniteHeightLattice.Known-⊤ fhl) where
+        open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_; isJoinSemilattice to isJoinSemilatticeᵇ; isMeetSemilattice to isMeetSemilatticeᵇ; isLattice to isLatticeᵇ)
+
+        open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong; x≼x⊔y to x≼ᵇx⊔ᵇy; ≼-antisym to ≼ᵇ-antisym; ⊔-Monotonicʳ to ⊔ᵇ-Monotonicʳ)
+
+        Elem : Set
+        Elem = Σ Node λ n → (proj₁ (𝓛 n))
+
+        LatticeT : Node → Set
+        LatticeT n = proj₁ (𝓛 n)
+
+        FHL : (n : Node) → FiniteHeightLattice (LatticeT n)
+        FHL n = proj₁ (proj₂ (𝓛 n))
+
+        ⊥≼x : ∀ {n : Node} (l : LatticeT n) → FiniteHeightLattice._≼_ (FHL n) (FiniteHeightLattice.⊥ (FHL n)) l
+        ⊥≼x {n} = proj₁ (proj₂ (proj₂ (𝓛 n)))
+
+        data _≈_ : Elem → Elem → Set where
+            ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} →
+                     FiniteHeightLattice._≈_ (FHL n) l₁ l₂ →
+                     (n , l₁) ≈ (n , l₂)
+
+        ≈-refl : ∀ {e : Elem} → e ≈ e
+        ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+
+        ≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁
+        ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (FHL n₁) l₁≈l₂)
+
+        ≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃
+        ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) l₁≈l₂ l₂≈l₃)
+
+        _⊔_ : Elem → Elem → Elem
+        _⊔_ e₁ e₂
+            using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
+            using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂)
+            where
+                select : ∀ n' e₁ e₂ → LatticeT n'
+                select n' (n₁ , l₁) (n₂ , l₂)
+                    with n' ≟ n₁ | n' ≟ n₂
+                ...   | yes refl | yes refl = FiniteHeightLattice._⊔_ (FHL n') l₁ l₂
+                ...   | yes refl | _ = l₁
+                ...   | _ | yes refl = l₂
+                ...   | no _ | no _ = FiniteHeightLattice.⊥ (FHL n')
+
+        ⊔-idemp : ∀ e → (e ⊔ e) ≈ e
+        ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
+            with n ≟ n
+        ...   | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (FHL n) l)
+        ...   | no n≢n = ⊥-elim (n≢n refl)
+
+        ⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁)
+        ⊔-comm (n₁ , l₁) (n₂ , l₂)
+            rewrite ⊔ᵇ-comm n₁ n₂
+            with n ← n₂ ⊔ᵇ n₁
+            with n ≟ n₁ | n ≟ n₂
+        ...   | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (FHL n) l₁ l₂)
+        ...   | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+        ...   | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
+
+        private
+            scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl)
+            scary n₁ n₂ refl with n₁ ≟ n₂
+            ... | yes refl = refl
+            ... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl)
+
+            payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃)
+                                    in LatticeT n
+            payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
+                with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
+            ...   | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃
+            ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
+            ...   | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
+            ...   | yes refl | no _ | no _ = l₁
+            ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
+            ...   | no _ | yes refl | no _ = l₂
+            ...   | no _ | no _ | yes refl = l₃
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
+
+            payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃))
+                                    in LatticeT n
+            payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃)
+                using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
+                with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
+            ...   | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃)
+            ...   | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
+            ...   | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
+            ...   | yes refl | no _ | no _ = l₁
+            ...   | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
+            ...   | no _ | yes refl | no _ = l₂
+            ...   | no _ | no _ | yes refl = l₃
+            ...   | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
+
+            ⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ →
+                                   (n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁)
+            ⊔ᵇ-prop n₁ n₂ n₃ pⁿ =
+                let n₁≼n₁⊔n₂ = x≼ᵇx⊔ᵇy n₁ n₂
+                    n₁⊔n₂≼n₁₂⊔n₃ = x≼ᵇx⊔ᵇy (n₁ ⊔ᵇ n₂) n₃
+                    n₁⊔n₂≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₂≼n₁₂⊔n₃)) pⁿ
+                    n₁⊔n₂≡n₁ = ≼ᵇ-antisym n₁⊔n₂≼n₁ n₁≼n₁⊔n₂
+                    n₁≼n₁⊔n₃ = x≼ᵇx⊔ᵇy n₁ n₃
+                    n₁⊔n₃≼n₁₂⊔n₃ = ⊔ᵇ-Monotonicʳ n₃ n₁≼n₁⊔n₂
+                    n₁⊔n₃≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₃≼n₁₂⊔n₃)) pⁿ
+                    n₁⊔n₃≡n₁ = ≼ᵇ-antisym n₁⊔n₃≼n₁ n₁≼n₁⊔n₃
+                in (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁)
+
+            Reassocˡ : ∀ e₁ e₂ e₃ →
+                      ((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ e₁ e₂ e₃)
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ
+                with n ≟ n₁ in d₁ | n ≟ n₂ in d₂ | n ≟ n₃ in d₃
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | yes refl
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | no _
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes p₁@refl | no n₁≢n₂ | yes p₃@refl
+                    using n₁⊔n₂≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₂})) (⊔ᵇ-assoc n₁ n₁ n₂)) (⊔ᵇ-comm n₁ (n₁ ⊔ᵇ n₂))) pⁿ
+                    with (n₁ ⊔ᵇ n₂) ≟ n₁
+            ...       | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁)
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...           | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...           | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...           | yes refl | no _ = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes p₁@refl | no n₁≢n₂ | no n₁≢n₃
+                    using (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁) ← ⊔ᵇ-prop n₁ n₂ n₃ pⁿ
+                    with n₁ ⊔ᵇ n₂ ≟ n₁
+            ...       | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁)
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...           | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...           | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...           | yes refl | no _ = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes p₂@refl | yes p₃@refl
+                    using n₁⊔n₂≡n₂ ← trans (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (sym (⊔ᵇ-idemp n₂))) (sym (⊔ᵇ-assoc n₁ n₂ n₂))) pⁿ
+                    with (n₁ ⊔ᵇ n₂) ≟ n₂
+            ...       | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ n₁⊔n₂≡n₂)
+            ...       | yes p rewrite p
+                        with n₂ ≟ n₁ | n₂ ≟ n₂
+            ...           | yes n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ n₂≡n₁)
+            ...           | _ | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...           | no _ | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes p₂@refl | no n₂≢n₃
+                    using (n₂⊔n₁≡n₂ , n₂⊔n₃≡n₂) ← ⊔ᵇ-prop n₂ n₁ n₃ (trans (≡-⊔ᵇ-cong (⊔ᵇ-comm n₂ n₁) (refl {x = n₃})) pⁿ)
+                    with (n₁ ⊔ᵇ n₂) ≟ n₁ | (n₁ ⊔ᵇ n₂) ≟ n₂
+            ...       | yes n₁⊔n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ (trans (sym n₂⊔n₁≡n₂) (trans (⊔ᵇ-comm n₂ n₁) (n₁⊔n₂≡n₁))))
+            ...       | _ | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ (trans (⊔ᵇ-comm n₁ n₂) n₂⊔n₁≡n₂))
+            ...       | no n₁⊔n₂≢n₁ | yes p rewrite p
+                        with n₂ ≟ n₂
+            ...           | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...           | yes refl = ≈-refl
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₃≢n₁ | no n₃≢n₂ | yes p₃@refl
+                    with n₁₂ ← n₁ ⊔ᵇ n₂
+                    with n₃ ≟ n₁₂
+            ...       | no n₃≢n₁₂ = ≈-refl
+            ...       | yes refl rewrite d₁ rewrite d₂ = ≈-lift (⊥≼x l₃) -- TODO: need ⊥ ⊔ n₃ ≡ n₃
+            Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n≢n₁ | no n≢n₂ | no n≢n₃
+                    with n₁₂ ← n₁ ⊔ᵇ n₂
+                    with n₁₂ ≟ n₁ | n₁₂ ≟ n₂ | n ≟ n₃ | n ≟ n₁₂
+            ...       | _ | _ | yes n≡n₃ | _ = ⊥-elim (n≢n₃ n≡n₃)
+            ...       | _ | _ | no _ | no n≢n₁₂ = ≈-refl
+            ...       | yes refl | yes refl | no _ | yes refl = ⊥-elim (n≢n₁ refl)
+            ...       | yes refl | no n₁₂≢n₂ | no _ | yes refl = ⊥-elim (n≢n₁ refl)
+            ...       | no n₁₂≢n₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | no _ | no _ | no _ | yes refl = ≈-refl
+
+            Reassocʳ : ∀ e₁ e₂ e₃ →
+                       (e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ e₁ e₂ e₃)
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃) in pⁿ
+                with n ≟ n₁ in d₁ | n ≟ n₂ in d₂ | n ≟ n₃ in d₃
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | yes refl
+                    with (n₁ ⊔ᵇ n₁) ≟ n₁
+            ...       | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
+            ...       | yes p rewrite p
+                        with n₁ ≟ n₁
+            ...           | no n₁≢n₁ = ⊥-elim (n₁≢n₁ refl)
+            ...           | yes refl = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | yes refl | no n₁≢n₃
+                    using n₁⊔n₃≡n₁ ← trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₃})) (trans (⊔ᵇ-assoc n₁ n₁ n₃) pⁿ)
+                    rewrite n₁⊔n₃≡n₁
+                    with n₁ ≟ n₁ | n₁ ≟ n₃
+            ...     | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...     | _ | yes n₁≡n₃ = ⊥-elim (n₁≢n₃ n₁≡n₃)
+            ...     | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | no n₁≢n₂ | yes refl
+                    using n₂⊔n₁≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (refl {x = n₂}) (sym (⊔ᵇ-idemp n₁))) (sym (⊔ᵇ-assoc n₂ n₁ n₁))) (⊔ᵇ-comm _ _)) pⁿ
+                    rewrite n₂⊔n₁≡n₁
+                    with n₁ ≟ n₁ | n₁ ≟ n₂
+            ...       | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl)
+            ...       | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
+            ...       | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | yes refl | no n₁≢n₂ | no n₁≢n₃
+                    with n₂₃ ← n₂ ⊔ᵇ n₃
+                    with n₁ ≟ n₂₃
+            ...       | no n₁≢n₂₃ = ≈-refl
+            ...       | yes refl rewrite d₂ rewrite d₃ = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) (FiniteHeightLattice.⊔-comm (FHL n₁) _ _) (⊥≼x l₁))
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes refl | yes refl
+                    rewrite ⊔ᵇ-idemp n₂
+                    with n₂ ≟ n₂
+            ...       | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
+            ...       | yes refl = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₂≢n₁ | yes refl | no n₂≢n₃
+                  using (n₂⊔n₃=n₂ , n₂⊔n₁=n₂) ← ⊔ᵇ-prop n₂ n₃ n₁ (trans (⊔ᵇ-comm _ _) pⁿ)
+                  rewrite n₂⊔n₃=n₂
+                  with n₂ ≟ n₂ | n₂ ≟ n₃
+            ...     | no n₂≢n₂ | _ = ⊥-elim (n₂≢n₂ refl)
+            ...     | _ | yes n₂≡n₃ = ⊥-elim (n₂≢n₃ n₂≡n₃)
+            ...     | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n₃≢n₁ | no n₃≢n₂ | yes refl
+                    using (n₃⊔n₂≡n₃ , n₃⊔n₁≡n₃) ← ⊔ᵇ-prop n₃ n₂ n₁ (trans (⊔ᵇ-comm _ _) (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (⊔ᵇ-comm n₃ n₂)) pⁿ))
+                    rewrite trans (⊔ᵇ-comm _ _) n₃⊔n₂≡n₃
+                    with n₃ ≟ n₃ | n₃ ≟ n₂
+            ...       | no n₃≢n₃ | _ = ⊥-elim (n₃≢n₃ refl)
+            ...       | _ | yes n₃≡n₂ = ⊥-elim (n₃≢n₂ n₃≡n₂)
+            ...       | yes refl | no _ = ≈-refl
+            Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
+                  | no n≢n₁ | no n≢n₂ | no n≢n₃
+                    with n₂₃ ← n₂ ⊔ᵇ n₃
+                    with n₂₃ ≟ n₂ | n₂₃ ≟ n₃ | n ≟ n₁ | n ≟ n₂₃
+            ...       | _ | _ | yes n≡n₁ | _ = ⊥-elim (n≢n₁ n≡n₁)
+            ...       | _ | _ | no _ | no _ = ≈-refl
+            ...       | yes refl | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | yes refl | no n₁₂≢n₂ | no _ | yes refl = ⊥-elim (n≢n₂ refl)
+            ...       | no n₁₂≢n₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₃ refl)
+            ...       | no n₁₂≢n₁ | no n₁₂≢n₂ | no _ | yes refl = ≈-refl
+
+
+        ⊔-assoc : ∀ (e₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃))
+        ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)
+            with nˡ ← proj₁ ((e₁ ⊔ e₂) ⊔ e₃) in pˡ
+            with nʳ ← proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) in pʳ
+            with final₁ ← Reassocˡ e₁ e₂ e₃
+            with final₂ ← Reassocʳ e₁ e₂ e₃
+            rewrite pˡ rewrite pʳ
+            rewrite ⊔ᵇ-assoc n₁ n₂ n₃
+            rewrite trans (sym pˡ ) pʳ
+            with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃
+        ...   | yes refl | yes refl | yes refl =
+            let l-assoc = FiniteHeightLattice.⊔-assoc (FHL n₁) l₁ l₂ l₃
+            in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂))
+        ...   | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | yes refl | no _ | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | yes refl | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
+        ...   | no _ | no _ | no _ = ≈-trans final₁ (≈-sym final₂)

Utils.agda

@@ -1,19 +1,32 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (_×_)
+open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat using (ℕ; suc)
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
-open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional using (_∈_; lose)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; all?; lookup)
+open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ; ++⁻ʳ)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
+open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (¬_; yes; no; Dec)
+open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Decidable)
 
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
+Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x)
+Decidable-¬ Decidable-P x = ¬? (Decidable-P x)
+
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
     push : ∀ {x : C} {xs : List C}
@@ -34,6 +47,24 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
+Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
+Unique-++⁻ˡ [] Unique-ys = empty
+Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
+
+Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
+Unique-++⁻ʳ [] Unique-ys = Unique-ys
+Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
+
+Unique-∈-++ˡ : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs → ¬ x ∈ ys
+Unique-∈-++ˡ [] _ ()
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push x≢xs++ys _) (here refl) = All¬-¬Any (++⁻ʳ xs x≢xs++ys)
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-∈-++ˡ xs Unique-xs++ys x̷∈xs
+
+Unique-narrow : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs →  Unique (x ∷ ys)
+Unique-narrow [] _ ()
+Unique-narrow {x = x} (x' ∷ xs) (push x≢xs++ys Unique-xs++ys) (here refl) = push (++⁻ʳ xs x≢xs++ys) (Unique-++⁻ʳ xs Unique-xs++ys)
+Unique-narrow {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-narrow xs Unique-xs++ys x̷∈xs
+
 All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
             All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
@@ -46,9 +77,8 @@ Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
 Unique-map {l = []} _ _ _ = empty
 Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
 
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
+¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
 
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
@@ -106,3 +136,42 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
+
+z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
+z≢sf f ()
+
+z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+z≢mapsfs [] = []
+z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+fins 0 = ([] , empty)
+fins (suc n') =
+    let
+        (inds' , unids') = fins n'
+    in
+        ( zero ∷ mapˡ suc inds'
+        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+        )
+
+fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
+fins-complete (suc n') zero = here refl
+fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))
+
+findUniversal : ∀ {p c} {C : Set c} {R : C → C → Set p} (l : List C) →  Decidable² R →
+                Dec (Any (λ x → All (R x) l) l)
+findUniversal l Rdec = any? (λ x → all? (Rdec x) l) l
+
+findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C) →
+                       Antisymmetric _≡_ R →
+                       ∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
+                       x₁ ≡ x₂
+findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)
+
+x∷xs≢[] : ∀ {a} {A : Set a} (x : A) (xs : List A) → ¬ (x ∷ xs ≡ [])
+x∷xs≢[] x xs ()
+
+foldr₁ : ∀ {a} {A : Set a} {l : List A} → ¬ (l ≡ []) → (A → A → A) → A
+foldr₁ {l = x ∷ []} _ _ = x
+foldr₁ {l = x ∷ x' ∷ xs} _ f = f x (foldr₁ {l = x' ∷ xs} (x∷xs≢[] x' xs) f)
+foldr₁ {l = []} l≢[] _ = ⊥-elim (l≢[] refl)