From e77c0ed9e6ec1d23c599079d6f0460609bccddcd Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Tue, 27 Jul 2021 07:41:02 +0200
Subject: [PATCH 1/6] second attempt at finite csp instance type

---
 UniversalAlgebra/Complexity/FiniteCSP.lagda | 138 ++++++++++++++++++++
 1 file changed, 138 insertions(+)
 create mode 100644 UniversalAlgebra/Complexity/FiniteCSP.lagda

diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
new file mode 100644
index 00000000..5235e1ab
--- /dev/null
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -0,0 +1,138 @@
+---
+layout: default
+title : Complexity.FiniteCSP module (The Agda Universal Algebra Library)
+date : 2021-07-26
+author: [agda-algebras development team][]
+---
+
+### Constraint Satisfaction Problems
+
+\begin{code}
+
+{-# OPTIONS --without-K --exact-split --safe #-}
+
+module Complexity.FiniteCSP  where
+
+open import Agda.Builtin.Equality using ( _≡_ ; refl )
+open import Data.Bool             using ( Bool ; true ; false ; _∧_)
+open import Data.Fin.Base         using ( Fin ; toℕ ; fromℕ ; raise)
+open import Data.Vec              using ( Vec ; [] ; tabulate ; lookup ; _∷_ ; map )
+open import Data.Vec.Relation.Unary.All using ( All )
+open import Data.Nat              using ( ℕ ; zero ; suc ; _+_ )
+
+open import Agda.Primitive   using ( _⊔_ ; lsuc ; Level) renaming ( Set to Type )
+open import Function.Base    using ( _∘_ )
+open import Relation.Binary  using ( DecSetoid)
+
+private variable
+ α ℓ : Level
+
+\end{code}
+
+#### Constraints
+
+We start with a vector (of length n, say) of variables.  For simplicity, we'll use the natural
+numbers for variable symbols, so
+
+V : Vec ℕ n
+V = [0 1 2 ... n-1]
+
+We can use the following range function to construct the vector of variables.
+
+\begin{code}
+
+range : (n : ℕ) → Vec ℕ n
+range n = tabulate toℕ
+-- `range n` is 0 ∷ 1 ∷ 2 ∷ … ∷ n-1 ∷ []
+
+\end{code}
+
+Let `nvar` denote the number of variables.
+
+A *constraint* consists of
+
+1. a natural number `∣s∣` denoting the number of variables in the "scope" of the constraint;
+
+2. a scope vector,  `s : Vec (Fin nvar) ∣s∣` , where `s i` is `k` if `k` is the i-th variable
+   in the scope of the constraint.
+
+3. a constraint relation, rel, which is a collection of functions mapping (indices of)
+   variables in the scope to elements of the domain.
+
+To summarize, a constraint is a triple (∣s∣ , s , rel), where
+* ∣s∣ is the number of variables in scope s.
+* s is the scope function: s i ≡ v iff v is the i-th variable in scope s.
+* rel is the contraint relation: a collection of functions mapping indices
+  of scope variables to elements in the domain.
+
+\begin{code}
+
+open DecSetoid
+open Fin renaming (zero to fzer ; suc to fsuc)
+
+record Constraint (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type α where
+ field
+  ∣s∣ : Fin nvar                     -- The "number" of variables involved in the constraint.
+  s : Vec (Fin nvar) (toℕ ∣s∣)        -- Vec of variables involved in the constraint.
+  rel : ((i : Fin (toℕ ∣s∣)) → Carrier ((lookup dom) (lookup s i))) →  Bool
+         -- `rel f` returns true iff the function f belongs to the relation
+
+ satisfies : (∀ i → Carrier ((lookup dom) i)) → Bool         -- An assignment f of values to variables
+ satisfies f = rel (λ (i : Fin (toℕ ∣s∣)) → f (lookup s i))  -- *satisfies* the constraint provided
+                                                             -- the function f, evaluated at each variable
+                                                             -- in the scope, belongs to the relation rel.
+
+
+-- utility functions --
+foldleft : ∀ {α β} {A : Type α} {B : Type β} {m} →
+           (B → A → B) → B → Vec A m → B
+foldleft _⊕_ b []       = b
+foldleft _⊕_ b (x ∷ xs) = foldleft _⊕_ (b ⊕ x) xs
+-- cf. stdlib's foldl, which seems harder to use than this one
+
+bool2nat : Bool → ℕ
+bool2nat false = 0
+bool2nat true = 1
+
+-- The number of elements of v that satisfy P
+countBool : {n : ℕ}{A : Set α} → Vec A n → (P : A → Bool) → ℕ
+countBool v P = foldleft _+_ 0 (map (bool2nat ∘ P) v)
+-- cf. stdlib's count, which works with general predicates (of type Pred A _)
+
+-- Return true iff all elements of v satisfy predicate P
+AllBool : ∀{n}{A : Set α} → Vec A n → (P : A → Bool) → Bool
+AllBool v P = foldleft _∧_ true (map P v)
+-- cf. stdlib's All, which works with general predicates (of type Pred A _)
+
+
+
+open Constraint
+record CSPInstance (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type α where
+ field
+  ncon : ℕ      -- the number of constraints involved
+  constr : Vec (Constraint nvar dom) ncon
+
+ -- f *solves* the instance if it satisfies all constraints.
+ isSolution :  (∀ i → Carrier ((lookup dom) i)) → Bool
+ isSolution f = AllBool constr P
+  where
+  P : Constraint nvar dom → Bool
+  P c = (satisfies c) f
+
+ -- A more general version...? (P is a more general Pred)
+ isSolution' :  (∀ i → Carrier ((lookup dom) i)) → Type α
+ isSolution' f = All P constr
+  where
+  P : Constraint nvar dom → Type
+  P c = (satisfies c) f ≡ true
+
+
+\end{code}
+
+
+
+--------------------------------------
+
+[agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team
+
+

From 105829f749de90b04501b92327e7c2b5abbdc382 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Wed, 28 Jul 2021 21:52:16 +0200
Subject: [PATCH 2/6] attempt to improve basic definitions for finite csp

---
 UniversalAlgebra/Complexity/FiniteCSP.lagda | 165 ++++++++++++--------
 1 file changed, 101 insertions(+), 64 deletions(-)

diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
index 5235e1ab..f38e7abb 100644
--- a/UniversalAlgebra/Complexity/FiniteCSP.lagda
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -13,22 +13,24 @@ author: [agda-algebras development team][]
 
 module Complexity.FiniteCSP  where
 
-open import Agda.Builtin.Equality using ( _≡_ ; refl )
-open import Data.Bool             using ( Bool ; true ; false ; _∧_)
-open import Data.Fin.Base         using ( Fin ; toℕ ; fromℕ ; raise)
-open import Data.Vec              using ( Vec ; [] ; tabulate ; lookup ; _∷_ ; map )
+open import Agda.Primitive        using ( _⊔_ ; lsuc ; Level) renaming ( Set to Type )
+open import Data.Bool             using ( Bool ; T? )
+open import Data.Bool.Base        using ( T )
+open import Data.Fin.Base         using ( Fin ; toℕ )
+open import Data.Product          using ( _,_ ; Σ-syntax ; _×_ )
+open import Data.Vec              using ( Vec ; lookup ; count ; tabulate )
 open import Data.Vec.Relation.Unary.All using ( All )
-open import Data.Nat              using ( ℕ ; zero ; suc ; _+_ )
-
-open import Agda.Primitive   using ( _⊔_ ; lsuc ; Level) renaming ( Set to Type )
-open import Function.Base    using ( _∘_ )
-open import Relation.Binary  using ( DecSetoid)
+open import Data.Nat              using ( ℕ )
+open import Function.Base         using ( _∘_ )
+open import Relation.Binary       using ( DecSetoid ; Rel )
+open import Relation.Unary        using ( Pred ; _∈_ )
 
 private variable
- α ℓ : Level
+ α ℓ ρ : Level
 
 \end{code}
 
+
 #### Constraints
 
 We start with a vector (of length n, say) of variables.  For simplicity, we'll use the natural
@@ -37,7 +39,7 @@ numbers for variable symbols, so
 V : Vec ℕ n
 V = [0 1 2 ... n-1]
 
-We can use the following range function to construct the vector of variables.
+We can use the following function to construct the vector of variables.
 
 \begin{code}
 
@@ -51,88 +53,123 @@ Let `nvar` denote the number of variables.
 
 A *constraint* consists of
 
-1. a natural number `∣s∣` denoting the number of variables in the "scope" of the constraint;
+1. a scope vector,  `s : Vec Bool nvar` , where `s i` is `true` if variable `i` is in the scope
+   of the constraint.
 
-2. a scope vector,  `s : Vec (Fin nvar) ∣s∣` , where `s i` is `k` if `k` is the i-th variable
-   in the scope of the constraint.
-
-3. a constraint relation, rel, which is a collection of functions mapping (indices of)
+2. a constraint relation, rel, which is a collection of functions mapping
    variables in the scope to elements of the domain.
 
-To summarize, a constraint is a triple (∣s∣ , s , rel), where
-* ∣s∣ is the number of variables in scope s.
-* s is the scope function: s i ≡ v iff v is the i-th variable in scope s.
-* rel is the contraint relation: a collection of functions mapping indices
-  of scope variables to elements in the domain.
-
 \begin{code}
 
-open DecSetoid
-open Fin renaming (zero to fzer ; suc to fsuc)
+-- syntactic sugar for vector element lookup
+_[_] : {A : Set α}{n : ℕ} → Vec A n → Fin n → A
+v [ i ] = (lookup v) i
 
-record Constraint (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type α where
- field
-  ∣s∣ : Fin nvar                     -- The "number" of variables involved in the constraint.
-  s : Vec (Fin nvar) (toℕ ∣s∣)        -- Vec of variables involved in the constraint.
-  rel : ((i : Fin (toℕ ∣s∣)) → Carrier ((lookup dom) (lookup s i))) →  Bool
-         -- `rel f` returns true iff the function f belongs to the relation
-
- satisfies : (∀ i → Carrier ((lookup dom) i)) → Bool         -- An assignment f of values to variables
- satisfies f = rel (λ (i : Fin (toℕ ∣s∣)) → f (lookup s i))  -- *satisfies* the constraint provided
-                                                             -- the function f, evaluated at each variable
-                                                             -- in the scope, belongs to the relation rel.
 
+open DecSetoid
 
--- utility functions --
-foldleft : ∀ {α β} {A : Type α} {B : Type β} {m} →
-           (B → A → B) → B → Vec A m → B
-foldleft _⊕_ b []       = b
-foldleft _⊕_ b (x ∷ xs) = foldleft _⊕_ (b ⊕ x) xs
--- cf. stdlib's foldl, which seems harder to use than this one
+-- {nvar : ℕ}{dom : Vec (DecSetoid α ℓ) nvar} → 
 
-bool2nat : Bool → ℕ
-bool2nat false = 0
-bool2nat true = 1
+record Constraint {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ) where
+ field
+  s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
+  rel : Pred (∀ i → Carrier (dom [ i ])) ρ -- some functions from `Fin nvar` to `dom`
 
--- The number of elements of v that satisfy P
-countBool : {n : ℕ}{A : Set α} → Vec A n → (P : A → Bool) → ℕ
-countBool v P = foldleft _+_ 0 (map (bool2nat ∘ P) v)
--- cf. stdlib's count, which works with general predicates (of type Pred A _)
+ -- scope size (i.e., # of vars involved in constraint)
+ ∣s∣ : ℕ
+ ∣s∣ = count T? s
 
--- Return true iff all elements of v satisfy predicate P
-AllBool : ∀{n}{A : Set α} → Vec A n → (P : A → Bool) → Bool
-AllBool v P = foldleft _∧_ true (map P v)
--- cf. stdlib's All, which works with general predicates (of type Pred A _)
+ -- point-wise equality of functions when restricted to the scope
+ _≐s_ : Rel (∀ i → Carrier (dom [ i ])) ℓ
+ f ≐s g = ∀ i → T (s [ i ]) → (dom [ i ])._≈_ (f i) (g i)
 
+ satisfies : (∀ i → Carrier (dom [ i ])) → Type (α ⊔ ℓ ⊔ ρ) -- An assignment f of values to variables
+ satisfies f = Σ[ g ∈ (∀ i → Carrier (dom [ i ])) ]         -- *satisfies* the constraint provided
+                ( (g ∈ rel) × f ≐s g )                        -- the function f, evaluated at each variable
+                                                             -- in the scope, belongs to the relation rel.
 
 
 open Constraint
-record CSPInstance (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type α where
+record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
  field
   ncon : ℕ      -- the number of constraints involved
-  constr : Vec (Constraint nvar dom) ncon
+  constr : Vec (Constraint {ρ = ρ} nvar dom) ncon
 
  -- f *solves* the instance if it satisfies all constraints.
- isSolution :  (∀ i → Carrier ((lookup dom) i)) → Bool
- isSolution f = AllBool constr P
+ isSolution :  (∀ i → Carrier (dom [ i ])) → Type _
+ isSolution f = All P constr
   where
-  P : Constraint nvar dom → Bool
+  P : Pred (Constraint nvar dom) _
   P c = (satisfies c) f
 
- -- A more general version...? (P is a more general Pred)
- isSolution' :  (∀ i → Carrier ((lookup dom) i)) → Type α
- isSolution' f = All P constr
-  where
-  P : Constraint nvar dom → Type
-  P c = (satisfies c) f ≡ true
-
 
 \end{code}
 
 
 
+Here's Jacques' nice explanation, comparing/contrasting a general predicate with a Bool-valued function:
+
+"A predicate maps to a whole type's worth of evidence that the predicate holds (or none
+at all if it doesn't). true just says it holds and absolutely nothing else. Bool is slightly
+different though, because a Bool-valued function is equivalent to a proof-irrelevant
+decidable predicate."
+
+
+
+
+
+
+
+
+
+
+
+
 --------------------------------------
 
 [agda-algebras development team]: https://github.com/ualib/agda-algebras#the-agda-algebras-development-team
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+-- Return true iff all elements of v satisfy predicate P
+-- AllBool : ∀{n}{A : Set α} → Vec A n → (P : A → Bool) → Bool
+-- AllBool v P = foldleft _∧_ true (map P v)
+-- cf. stdlib's All, which works with general predicates (of type Pred A _)
+
+
+ -- A more general version...? (P is a more general Pred)
+ -- isSolution' :  (∀ i → Carrier ((lookup dom) i)) → Type α
+ -- isSolution' f = All P constr
+ --  where
+ --  P : Constraint nvar dom → Type
+ --  P c = (satisfies c) f ≡ true
+
+-- bool2nat : Bool → ℕ
+-- bool2nat false = 0
+-- bool2nat true = 1
+
+
+-- The number of elements of v that satisfy P
+-- countBool : {n : ℕ}{A : Set α} → Vec A n → (P : A → Bool) → ℕ
+-- countBool v P = foldl (λ _ → ℕ) _+_ 0 (map (bool2nat ∘ P) v)
+

From bb8f3b60c51bf4d54bce661e8fbc943f2bad6302 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sat, 31 Jul 2021 11:23:09 +0200
Subject: [PATCH 3/6] improvements

---
 UniversalAlgebra/Complexity/FiniteCSP.lagda   | 33 ++++---
 UniversalAlgebra/Foundations/Truncation.lagda |  3 +
 .../Foundations/Welldefined.lagda             | 67 +++++++++++++-
 UniversalAlgebra/Overture/Transformers.lagda  | 87 +++++++++++++++----
 4 files changed, 162 insertions(+), 28 deletions(-)

diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
index f38e7abb..160ba239 100644
--- a/UniversalAlgebra/Complexity/FiniteCSP.lagda
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -14,9 +14,11 @@ author: [agda-algebras development team][]
 module Complexity.FiniteCSP  where
 
 open import Agda.Primitive        using ( _⊔_ ; lsuc ; Level) renaming ( Set to Type )
-open import Data.Bool             using ( Bool ; T? )
+open import Agda.Builtin.List     using (List; []; _∷_)
+open import Data.Bool             using ( Bool ; T? ; true)
 open import Data.Bool.Base        using ( T )
 open import Data.Fin.Base         using ( Fin ; toℕ )
+open import Data.List.Base        using ( length ; [_] ; _++_; head ; tail ; all) renaming (lookup to get)
 open import Data.Product          using ( _,_ ; Σ-syntax ; _×_ )
 open import Data.Vec              using ( Vec ; lookup ; count ; tabulate )
 open import Data.Vec.Relation.Unary.All using ( All )
@@ -62,8 +64,8 @@ A *constraint* consists of
 \begin{code}
 
 -- syntactic sugar for vector element lookup
-_[_] : {A : Set α}{n : ℕ} → Vec A n → Fin n → A
-v [ i ] = (lookup v) i
+_⟨_⟩ : {A : Set α}{n : ℕ} → Vec A n → Fin n → A
+v ⟨ i ⟩ = (lookup v) i
 
 
 open DecSetoid
@@ -73,22 +75,21 @@ open DecSetoid
 record Constraint {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ) where
  field
   s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
-  rel : Pred (∀ i → Carrier (dom [ i ])) ρ -- some functions from `Fin nvar` to `dom`
+  rel : Pred (∀ i → Carrier (dom ⟨ i ⟩)) ρ -- some functions from `Fin nvar` to `dom`
 
  -- scope size (i.e., # of vars involved in constraint)
  ∣s∣ : ℕ
  ∣s∣ = count T? s
 
  -- point-wise equality of functions when restricted to the scope
- _≐s_ : Rel (∀ i → Carrier (dom [ i ])) ℓ
- f ≐s g = ∀ i → T (s [ i ]) → (dom [ i ])._≈_ (f i) (g i)
+ _≐s_ : Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
+ f ≐s g = ∀ i → T (s ⟨ i ⟩) → (dom ⟨ i ⟩)._≈_ (f i) (g i)
 
- satisfies : (∀ i → Carrier (dom [ i ])) → Type (α ⊔ ℓ ⊔ ρ) -- An assignment f of values to variables
- satisfies f = Σ[ g ∈ (∀ i → Carrier (dom [ i ])) ]         -- *satisfies* the constraint provided
+ satisfies : (∀ i → Carrier (dom ⟨ i ⟩)) → Type (α ⊔ ℓ ⊔ ρ) -- An assignment f of values to variables
+ satisfies f = Σ[ g ∈ (∀ i → Carrier (dom ⟨ i ⟩)) ]         -- *satisfies* the constraint provided
                 ( (g ∈ rel) × f ≐s g )                        -- the function f, evaluated at each variable
                                                              -- in the scope, belongs to the relation rel.
 
-
 open Constraint
 record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
  field
@@ -96,13 +97,25 @@ record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar)
   constr : Vec (Constraint {ρ = ρ} nvar dom) ncon
 
  -- f *solves* the instance if it satisfies all constraints.
- isSolution :  (∀ i → Carrier (dom [ i ])) → Type _
+ isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Type _
  isSolution f = All P constr
   where
   P : Pred (Constraint nvar dom) _
   P c = (satisfies c) f
 
 
+record CSPInstanceList {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
+ field
+  constr : List (Constraint {ρ = ρ} nvar dom)
+
+ -- f *solves* the instance if it satisfies all constraints.
+ isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Bool
+ isSolution f = all P constr
+  where
+  P : (Constraint nvar dom) → Bool
+  P c = {!!} -- (satisfies c) f → 
+
+
 \end{code}
 
 
diff --git a/UniversalAlgebra/Foundations/Truncation.lagda b/UniversalAlgebra/Foundations/Truncation.lagda
index f14e5c8e..3b3ce080 100644
--- a/UniversalAlgebra/Foundations/Truncation.lagda
+++ b/UniversalAlgebra/Foundations/Truncation.lagda
@@ -69,6 +69,9 @@ is-prop-valued  _≈_ = ∀ x y → is-prop (x ≈ y)
 singleton-is-prop : {α : Level}(X : Type α) → is-singleton X → is-prop X
 singleton-is-prop X (c , φ) x y = x ≡⟨ (φ x)⁻¹ ⟩ c ≡⟨ φ y ⟩ y ∎
 
+is-inhabited : Type α → Type (lsuc α)
+is-inhabited {α = α} X = (P : Type α ) → is-prop P → (X → P) → P
+
 \end{code}
 
 
diff --git a/UniversalAlgebra/Foundations/Welldefined.lagda b/UniversalAlgebra/Foundations/Welldefined.lagda
index 782133f8..f4f278e8 100644
--- a/UniversalAlgebra/Foundations/Welldefined.lagda
+++ b/UniversalAlgebra/Foundations/Welldefined.lagda
@@ -12,12 +12,18 @@ author: [agda-algebras development team][]
 module Foundations.Welldefined where
 
 open import Agda.Builtin.Equality using (_≡_; refl)
+open import Agda.Builtin.List     using (List; []; _∷_)
 open import Agda.Primitive        using ( _⊔_ ; lsuc ; Level ) renaming ( Set to Type ; Setω to Typeω )
 open import Axiom.Extensionality.Propositional
                                   using () renaming ( Extensionality to funext )
-open import Data.Fin.Base         using ( Fin )
+open import Data.Fin.Base         using ( Fin ; toℕ)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
 open import Data.Product                using ( _,_ ; _×_ )
+open import Data.List.Base        using ( lookup ; length ; [_] ; _++_; head ; tail)
+open import Data.List.Properties  using ( ≡-dec )
 open import Function.Base         using ( _$_ ; _∘_ ; id )
+open import Relation.Binary       using ( Rel )
+open import Relation.Binary.Definitions  using ( DecidableEquality )
 import Relation.Binary.PropositionalEquality as PE
 
 
@@ -28,7 +34,7 @@ open import Overture.Transformers  using ( CurryFin2 ; UncurryFin2 ; UncurryFin3
                                          ; A×A~Fin2A-pointwise ; A→A~Fin2A-pointwise )
 
 private variable
- ι α β 𝓥 : Level
+ ι α β 𝓥 ρ : Level
 
 \end{code}
 
@@ -164,6 +170,7 @@ so f is essentially of type (Fin 2 → A) → B.
 
 \begin{code}
 
+
 module _ {A : Type α}{B : Type β} where
 
  open Fin renaming ( zero to z ; suc to s )
@@ -205,6 +212,28 @@ module _ {A : Type α}{B : Type β} where
          f (v z) (v (s z)) ≡⟨ refl ⟩
          (UncurryFin2 f) v ∎
 
+ -- Fin2-wd' : (f : (List A) → B)(u v : List A)
+ --  →        (all ∀ i → (loou ≈ v → f u ≡ f v
+
+ -- Fin2-wd' f u v u≈v = {!!}
+  -- where
+  -- zip1 : ∀ {a x y} → x ≡ y → f a x ≡ f a y
+  -- zip1 refl = refl
+  -- Goal : f u ≡ f v
+  -- Goal = {!!}
+  -- zip1 : ∀ {a x y} → x ≡ y → f a x ≡ f a y
+  -- zip1 refl = refl
+
+  -- zip2 : ∀ {x y b} → x ≡ y → f x b ≡ f y b
+  -- zip2 refl = refl
+
+  -- Goal : f (λ {z → u z ; (s z) → u (s z)}) ≡ f (λ {z → v z ; (s z) → v (s z)})
+  -- Goal = {!!} -- f (λ {z → u z ; (s z) → u (s z)}) ≡⟨ {!!} ⟩ 
+         -- (CurryFin2 f) (u z) (u (s z)) ≡⟨ {!!} ⟩ -- zip1 (u≈v (s z)) ⟩
+         -- (CurryFin2 f) (u z) (v (s z)) ≡⟨ {!!} ⟩ -- zip2 (u≈v z) ⟩
+         -- (CurryFin2 f) (v z) (v (s z)) ≡⟨ {!!} ⟩
+         -- f (λ {z → v z ; (s z) → v (s z) }) ∎
+
 
 
 
@@ -234,6 +263,40 @@ module _ {A : Type α}{B : Type β} where
 
  -- NEXT: try to prove (f : (Fin 2 → A) → B)(u v : Fin 2 → A) →  u ≈ v → f u ≡ f v
 
+module _ {A : Type α}{B : Type β} where -- {de : DecidableEquality A} where
+
+ ListA→B : (f : List A → B)(u v : List A)
+  →        u ≡ v → f u ≡ f v
+ ListA→B f u .u refl = refl
+
+ -- lookup⁻ : length xs ≡ length ys →
+ --          (∀ {i j} → toℕ i ≡ toℕ j → R (lookup xs i) (lookup ys j)) →
+ --          Pointwise R xs ys
+ -- →        ( ∀ i j → i ≡ j → (lookup u) i ≡ (lookup v) j )
+
+ CurryListA : (List A → B) → (List A → A → B)
+ CurryListA f [] a = f [ a ]
+ CurryListA f (x ∷ l) a = f ((x ∷ l) ++ [ a ]) 
+
+ CurryListA' : (List A → B) → (A → List A → B)
+ CurryListA' f a [] = f [ a ]
+ CurryListA' f a (x ∷ l) = f ([ a ] ++ (x ∷ l))
+
+
+ ListA→B-dec : (f : List A → B)(u v : List A)
+  →        (length u) ≡ (length v)
+  →        ( ∀ {i j} → toℕ i ≡ toℕ j → (lookup u i) ≡ (lookup v j ))
+  →        f u ≡ f v
+ ListA→B-dec f u v x y = {!Goal!}
+  where
+  zip1 : (CurryListA' f) (head u) (tail u) ≡ f u
+  zip1 = ?
+  Goal : f u ≡ f v
+  Goal = {!!}
+
+
+
+
 \end{code}
 
 
diff --git a/UniversalAlgebra/Overture/Transformers.lagda b/UniversalAlgebra/Overture/Transformers.lagda
index a7b198c4..242fe833 100644
--- a/UniversalAlgebra/Overture/Transformers.lagda
+++ b/UniversalAlgebra/Overture/Transformers.lagda
@@ -22,6 +22,7 @@ open import Agda.Primitive              using ( _⊔_ ; lsuc ; Level ) renaming
 open import Data.Product                using ( _,_ ; _×_ )
 open import Data.Fin.Base               using ( Fin )
 open import Function.Base               using ( _∘_ ; id )
+import Relation.Binary.PropositionalEquality as PE
 
 -- Imports from agda-algebras
 open import Overture.Preliminaries using ( _≈_ )
@@ -85,24 +86,9 @@ module _ {A : Type α} {B : Type β} where
 
 \begin{code}
 
-open Fin renaming (zero to z ; suc to s)
-
 module _ {A : Type α} where
 
- A→A→Fin2A : A → A → Fin 2 → A
- A→A→Fin2A x y z = x
- A→A→Fin2A x y (s _) = y
-
- A→A→Fin2A' : A → A → Fin 2 → A
- A→A→Fin2A' x y = u
-  where
-  u : Fin 2 → A
-  u z = x
-  u (s z) = y
-
- A→A→Fin2A-pointwise-agreement : (x y : A) → ∀ i → (A→A→Fin2A x y) i ≡ (A→A→Fin2A' x y) i
- A→A→Fin2A-pointwise-agreement x y z = refl
- A→A→Fin2A-pointwise-agreement x y (s z) = refl
+ open Fin renaming (zero to z ; suc to s)
 
  A×A→Fin2A : A × A → Fin 2 → A
  A×A→Fin2A (x , y) z = x
@@ -118,6 +104,21 @@ module _ {A : Type α} where
  A×A~Fin2A-pointwise u z = refl
  A×A~Fin2A-pointwise u (s z) = refl
 
+ A→A→Fin2A : A → A → Fin 2 → A
+ A→A→Fin2A x y z = x
+ A→A→Fin2A x y (s _) = y
+
+ A→A→Fin2A' : A → A → Fin 2 → A
+ A→A→Fin2A' x y = u
+  where
+  u : Fin 2 → A
+  u z = x
+  u (s z) = y
+
+ A→A→Fin2A-pointwise-agreement : (x y : A) → ∀ i → (A→A→Fin2A x y) i ≡ (A→A→Fin2A' x y) i
+ A→A→Fin2A-pointwise-agreement x y z = refl
+ A→A→Fin2A-pointwise-agreement x y (s z) = refl
+
  A→A~Fin2A-pointwise : (v : Fin 2 → A) → ∀ i → A→A→Fin2A (v z) (v (s z)) i ≡ v i
  A→A~Fin2A-pointwise v z = refl
  A→A~Fin2A-pointwise v (s z) = refl
@@ -141,6 +142,12 @@ function types, `(Fin 2 → A) → B` and `A × A → B`, nor between the types
 
 module _ {A : Type α} {B : Type β} where
 
+ open Fin renaming (zero to z ; suc to s)
+
+ lemma : (u : Fin 2 → A) → u ≈ (λ {z → u z ; (s z) → u (s z)})
+ lemma u z = refl
+ lemma u (s z) = refl
+
  CurryFin2 : ((Fin 2 → A) → B) → A → A → B
  CurryFin2 f x y = f (A→A→Fin2A x y)
 
@@ -150,6 +157,21 @@ module _ {A : Type α} {B : Type β} where
  CurryFin2~UncurryFin2 : CurryFin2 ∘ UncurryFin2 ≡ id
  CurryFin2~UncurryFin2 = refl
 
+ open PE.≡-Reasoning
+ -- UncurryFin2~CurryFin2 : ∀ f u → (UncurryFin2 ∘ CurryFin2) f u ≡ f u
+ -- UncurryFin2~CurryFin2 f u = Goal
+ --  where
+ --  -- Equiv Goal: (λ u → f (A→A→Fin2A (u z) (u (s z)))) ≡ f
+ --  Goal : (UncurryFin2 ∘ CurryFin2) f u ≡ f u
+ --  Goal = (UncurryFin2 ∘ CurryFin2) f u ≡⟨ refl ⟩
+ --         UncurryFin2 (λ x y → (f (A→A→Fin2A x y))) u ≡⟨ refl ⟩
+ --         (λ x y → (f (A→A→Fin2A x y))) (u z) (u (s z)) ≡⟨ refl ⟩
+ --         f (A→A→Fin2A (u z) (u (s z))) ≡⟨ PE.cong f {!!} ⟩
+ --         f (λ {z → u z ; (s z) → u (s z)}) ≡⟨ PE.cong f {!!} ⟩
+ --         f u ∎
+
+
+
  CurryFin3 : {A : Type α} → ((Fin 3 → A) → B) → A → A → A → B
  CurryFin3 {A = A} f x₁ x₂ x₃ = f u
   where
@@ -170,6 +192,39 @@ module _ {A : Type α} {B : Type β} where
  Fin2A→B~A×A→B : Fin2A→B-to-A×A→B ∘ A×A→B-to-Fin2A→B ≡ id
  Fin2A→B~A×A→B = refl
 
+ -- open PE.≡-Reasoning
+ -- A×A→B~Fin2A→B : ∀ f → (A×A→B-to-Fin2A→B ∘ Fin2A→B-to-A×A→B) f ≈ f
+ -- A×A→B~Fin2A→B f u = Goal
+ --  where
+ --  Goal : (A×A→B-to-Fin2A→B ∘ Fin2A→B-to-A×A→B) f u ≡ f u
+ --  Goal = (A×A→B-to-Fin2A→B ∘ Fin2A→B-to-A×A→B) f u ≡⟨ refl ⟩
+ --         A×A→B-to-Fin2A→B (f ∘ A×A→Fin2A) u ≡⟨ refl ⟩
+ --         ((f ∘ A×A→Fin2A) ∘ Fin2A→A×A) u ≡⟨ refl ⟩
+ --         f (A×A→Fin2A (Fin2A→A×A u)) ≡⟨ {!!} ⟩
+ --         f (λ { 𝟚.𝟎 → (A×A→Fin2A (Fin2A→A×A u)) 𝟚.𝟎 ; 𝟚.𝟏 → (A×A→Fin2A (Fin2A→A×A u)) 𝟚.𝟏 }) ≡⟨ {!!} ⟩
+ --         f u ∎
+
+
+
+ -- A×A→Fin2A : A × A → Fin 2 → A
+ -- A×A→Fin2A (x , y) z = x
+ -- A×A→Fin2A (x , y) (s z) = y
+
+ -- Fin2A→A×A : (Fin 2 → A) → A × A
+ -- Fin2A→A×A u = u z , u (s z)
+
+ -- Fin2A~A×A : {A : Type α} → Fin2A→A×A ∘ A×A→Fin2A ≡ id
+ -- Fin2A~A×A = refl
+
+ -- A×A~Fin2A-pointwise : ∀ u → (A×A→Fin2A (Fin2A→A×A u)) ≈ u
+ -- A×A~Fin2A-pointwise u z = refl
+ -- A×A~Fin2A-pointwise u (s z) = refl
+
+ -- A→A~Fin2A-pointwise : (v : Fin 2 → A) → ∀ i → A→A→Fin2A (v z) (v (s z)) i ≡ v i
+ -- A→A~Fin2A-pointwise v z = refl
+ -- A→A~Fin2A-pointwise v (s z) = refl
+
+
 \end{code}
 
 

From 2c35314b8337c1c08393c0856be6fa3fdd985789 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sat, 31 Jul 2021 21:11:34 +0200
Subject: [PATCH 4/6] minor mods

---
 UniversalAlgebra/Algebras/Basic.lagda       | 14 --------------
 UniversalAlgebra/Complexity/FiniteCSP.lagda | 18 ++++++++++++++----
 2 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/UniversalAlgebra/Algebras/Basic.lagda b/UniversalAlgebra/Algebras/Basic.lagda
index 8eed1753..2067c4b8 100644
--- a/UniversalAlgebra/Algebras/Basic.lagda
+++ b/UniversalAlgebra/Algebras/Basic.lagda
@@ -76,20 +76,6 @@ As mentioned earlier, throughout the [UniversalAlgebra][] library `𝓞` denote
 In the [Overture][] module we defined special syntax for the first and second projections---namely, ∣\_∣ and ∥\_∥, resp. Consequently, if `𝑆 : Signature 𝓞 𝓥` is a signature, then ∣ 𝑆 ∣ denotes the set of operation symbols, and ∥ 𝑆 ∥ denotes the arity function. If 𝑓 : ∣ 𝑆 ∣ is an operation symbol in the signature 𝑆, then ∥ 𝑆 ∥ 𝑓 is the arity of 𝑓.
 
 
-**Example (Monoid)**. Here is how we could define the signature for monoids as a member of the type `Signature 𝓞 𝓥`.
-
-\begin{code}
-
-data monoid-op {𝓞 : Level} : Type 𝓞 where
- e : monoid-op; · : monoid-op
-
-monoid-sig : Signature 𝓞 ℓ₀
-monoid-sig = monoid-op , λ { e → ⊥; · → Bool }
-
-\end{code}
-
-Thus, the signature for a monoid consists of two operation symbols, `e` and `·`, and a function `λ { e → 𝟘; · → 𝟚 }` which maps `e` to the empty type 𝟘 (since `e` is the nullary identity) and maps `·` to the two element type 𝟚 (since `·` is binary).
-
 
 #### <a id="algebras">Algebras</a>
 
diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
index 160ba239..6f2048d4 100644
--- a/UniversalAlgebra/Complexity/FiniteCSP.lagda
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -16,7 +16,7 @@ module Complexity.FiniteCSP  where
 open import Agda.Primitive        using ( _⊔_ ; lsuc ; Level) renaming ( Set to Type )
 open import Agda.Builtin.List     using (List; []; _∷_)
 open import Data.Bool             using ( Bool ; T? ; true)
-open import Data.Bool.Base        using ( T )
+open import Data.Bool.Base        using ( T ; _∧_ )
 open import Data.Fin.Base         using ( Fin ; toℕ )
 open import Data.List.Base        using ( length ; [_] ; _++_; head ; tail ; all) renaming (lookup to get)
 open import Data.Product          using ( _,_ ; Σ-syntax ; _×_ )
@@ -25,7 +25,8 @@ open import Data.Vec.Relation.Unary.All using ( All )
 open import Data.Nat              using ( ℕ )
 open import Function.Base         using ( _∘_ )
 open import Relation.Binary       using ( DecSetoid ; Rel )
-open import Relation.Unary        using ( Pred ; _∈_ )
+open import Relation.Nullary      using ( Dec )
+open import Relation.Unary        using ( Pred ; _∈_ ; Decidable )
 
 private variable
  α ℓ ρ : Level
@@ -72,10 +73,13 @@ open DecSetoid
 
 -- {nvar : ℕ}{dom : Vec (DecSetoid α ℓ) nvar} → 
 
+open Dec
+
 record Constraint {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ) where
  field
   s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
   rel : Pred (∀ i → Carrier (dom ⟨ i ⟩)) ρ -- some functions from `Fin nvar` to `dom`
+  dec : Decidable rel
 
  -- scope size (i.e., # of vars involved in constraint)
  ∣s∣ : ℕ
@@ -90,7 +94,11 @@ record Constraint {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar)
                 ( (g ∈ rel) × f ≐s g )                        -- the function f, evaluated at each variable
                                                              -- in the scope, belongs to the relation rel.
 
+ satisfies? : (f : ∀ i → Carrier (dom ⟨ i ⟩)) → Dec (satisfies f) -- Type (α ⊔ ℓ ⊔ ρ)
+ satisfies? f = {!!}
+
 open Constraint
+
 record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
  field
   ncon : ℕ      -- the number of constraints involved
@@ -104,7 +112,9 @@ record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar)
   P c = (satisfies c) f
 
 
-record CSPInstanceList {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
+record CSPInstanceList {ρ : Level}
+                       (nvar : ℕ)
+                       (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
  field
   constr : List (Constraint {ρ = ρ} nvar dom)
 
@@ -113,7 +123,7 @@ record CSPInstanceList {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) n
  isSolution f = all P constr
   where
   P : (Constraint nvar dom) → Bool
-  P c = {!!} -- (satisfies c) f → 
+  P c = does ((satisfies? c) f) -- (satisfies c) f → 
 
 
 \end{code}

From 78d0c711ad5ad9a7b18195b494e9cadf5d762299 Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sun, 1 Aug 2021 13:24:19 +0200
Subject: [PATCH 5/6] improvements

---
 UniversalAlgebra/Complexity/FiniteCSP.lagda | 24 ++++++++++++---------
 1 file changed, 14 insertions(+), 10 deletions(-)

diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
index 6f2048d4..42053c1e 100644
--- a/UniversalAlgebra/Complexity/FiniteCSP.lagda
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -75,20 +75,24 @@ open DecSetoid
 
 open Dec
 
-record Constraint {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ) where
- field
-  s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
-  rel : Pred (∀ i → Carrier (dom ⟨ i ⟩)) ρ -- some functions from `Fin nvar` to `dom`
-  dec : Decidable rel
+module CSPInstance
+ (nvar : ℕ)
+ (dom : Vec (DecSetoid α ℓ) nvar)
+
+ -- point-wise equality of functions when restricted to a scope
+ _≐s_ : {s : Vec Bool nvar} → Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
+ f ≐s g = ∀ i → T (s ⟨ i ⟩) → (dom ⟨ i ⟩)._≈_ (f i) (g i)
+
+ record Constraint {ρ : Level} : Type (α ⊔ lsuc ρ) where
+  field
+   s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
+   rel : Pred (∀ i → Carrier (dom ⟨ i ⟩)) ρ -- some functions from `Fin nvar` to `dom`
+   dec : Decidable rel
 
  -- scope size (i.e., # of vars involved in constraint)
  ∣s∣ : ℕ
  ∣s∣ = count T? s
 
- -- point-wise equality of functions when restricted to the scope
- _≐s_ : Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
- f ≐s g = ∀ i → T (s ⟨ i ⟩) → (dom ⟨ i ⟩)._≈_ (f i) (g i)
-
  satisfies : (∀ i → Carrier (dom ⟨ i ⟩)) → Type (α ⊔ ℓ ⊔ ρ) -- An assignment f of values to variables
  satisfies f = Σ[ g ∈ (∀ i → Carrier (dom ⟨ i ⟩)) ]         -- *satisfies* the constraint provided
                 ( (g ∈ rel) × f ≐s g )                        -- the function f, evaluated at each variable
@@ -123,7 +127,7 @@ record CSPInstanceList {ρ : Level}
  isSolution f = all P constr
   where
   P : (Constraint nvar dom) → Bool
-  P c = does ((satisfies? c) f) -- (satisfies c) f → 
+  P c = does ((satisfies? c) f)
 
 
 \end{code}

From ac5d42bd97e66f00e99b4841b6cf7fa93f59233d Mon Sep 17 00:00:00 2001
From: William DeMeo <williamdemeo@gmail.com>
Date: Sun, 1 Aug 2021 22:27:30 +0200
Subject: [PATCH 6/6] still working on it...
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

...but at least I now know a little bit more about `Prop`, `Bool`, and `Dec`.

**Question**. Suppose

```agda
∀ i → Dec (f i ≈ g i)
```

and suppose we define

```agda
f ≐ g = ∀ i → f i ≈ g i
```

Can we then prove `Dec (f ≐ g)`?

(That's what we need in the hole on line 142, and that what I'm trying to do in
lines 129--134.  I have the `Bool` part, but I still need the `Reflects (f ≐ g)` part.)
---
 UniversalAlgebra/Complexity/FiniteCSP.lagda | 142 +++++++++++++-------
 1 file changed, 97 insertions(+), 45 deletions(-)

diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
index 42053c1e..b3d9eb8b 100644
--- a/UniversalAlgebra/Complexity/FiniteCSP.lagda
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -1,4 +1,4 @@
----
+n---
 layout: default
 title : Complexity.FiniteCSP module (The Agda Universal Algebra Library)
 date : 2021-07-26
@@ -17,16 +17,22 @@ open import Agda.Primitive        using ( _⊔_ ; lsuc ; Level) renaming ( Set t
 open import Agda.Builtin.List     using (List; []; _∷_)
 open import Data.Bool             using ( Bool ; T? ; true)
 open import Data.Bool.Base        using ( T ; _∧_ )
-open import Data.Fin.Base         using ( Fin ; toℕ )
-open import Data.List.Base        using ( length ; [_] ; _++_; head ; tail ; all) renaming (lookup to get)
-open import Data.Product          using ( _,_ ; Σ-syntax ; _×_ )
-open import Data.Vec              using ( Vec ; lookup ; count ; tabulate )
+open import Data.Fin.Base         using ( Fin ; toℕ ; fold′ ; fromℕ ; raise )
+open import Data.List.Base        using ( [_] ; _++_; head ; tail ; all) renaming (lookup to get)
+open import Data.Product          using ( _,_ ; Σ-syntax ; _×_ ) renaming ( proj₁ to fst ; proj₂ to snd )
+open import Data.Vec              using ( Vec ; lookup ; filter ; zip )
+open import Data.Vec.Base         using ( allFin ; count ; tabulate ) renaming (length to vlength)
+open import Data.Vec.Bounded.Base using ( Vec≤ )
 open import Data.Vec.Relation.Unary.All using ( All )
-open import Data.Nat              using ( ℕ )
+open import Data.Nat              using ( ℕ ; zero ; suc )
 open import Function.Base         using ( _∘_ )
 open import Relation.Binary       using ( DecSetoid ; Rel )
-open import Relation.Nullary      using ( Dec )
-open import Relation.Unary        using ( Pred ; _∈_ ; Decidable )
+open import Relation.Binary.Structures using ( IsDecEquivalence )
+open import Relation.Nullary      using ( Dec ; _because_ ; Reflects )
+open import Relation.Unary        using ( Pred ; _∈_ ; Decidable ; ⋂ )
+
+open import Overture.Preliminaries using ( Π-syntax )
+
 
 private variable
  α ℓ ρ : Level
@@ -48,6 +54,8 @@ We can use the following function to construct the vector of variables.
 
 range : (n : ℕ) → Vec ℕ n
 range n = tabulate toℕ
+
+
 -- `range n` is 0 ∷ 1 ∷ 2 ∷ … ∷ n-1 ∷ []
 
 \end{code}
@@ -75,59 +83,103 @@ open DecSetoid
 
 open Dec
 
-module CSPInstance
- (nvar : ℕ)
- (dom : Vec (DecSetoid α ℓ) nvar)
+module finite-csp
+ {ρ : Level}
+ (nvar' : ℕ)
+ (dom : Vec (DecSetoid α ℓ) (suc nvar')) where
+
+ private
+  nvar = suc nvar'
 
- -- point-wise equality of functions when restricted to a scope
- _≐s_ : {s : Vec Bool nvar} → Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
- f ≐s g = ∀ i → T (s ⟨ i ⟩) → (dom ⟨ i ⟩)._≈_ (f i) (g i)
+ open Vec≤
 
- record Constraint {ρ : Level} : Type (α ⊔ lsuc ρ) where
+ record Constraint : Type (α ⊔ lsuc ρ) where
   field
    s   : Vec Bool nvar        -- entry i is true iff variable i is in scope
    rel : Pred (∀ i → Carrier (dom ⟨ i ⟩)) ρ -- some functions from `Fin nvar` to `dom`
    dec : Decidable rel
 
- -- scope size (i.e., # of vars involved in constraint)
- ∣s∣ : ℕ
- ∣s∣ = count T? s
+  -- scope size (i.e., # of vars involved in constraint)
+  ∣s∣ : ℕ
+  ∣s∣ = count T? s
 
- satisfies : (∀ i → Carrier (dom ⟨ i ⟩)) → Type (α ⊔ ℓ ⊔ ρ) -- An assignment f of values to variables
- satisfies f = Σ[ g ∈ (∀ i → Carrier (dom ⟨ i ⟩)) ]         -- *satisfies* the constraint provided
-                ( (g ∈ rel) × f ≐s g )                        -- the function f, evaluated at each variable
-                                                             -- in the scope, belongs to the relation rel.
+  -- variables symbols (i.e., 0, 1, ..., nvar -1) zipped with true/false values from s
+  i&s : Vec (Fin nvar × Bool) nvar
+  i&s = zip (allFin nvar) s
 
- satisfies? : (f : ∀ i → Carrier (dom ⟨ i ⟩)) → Dec (satisfies f) -- Type (α ⊔ ℓ ⊔ ρ)
- satisfies? f = {!!}
+  -- variables in scope along with T in second coordinate
+  sfT : Vec (Fin nvar × Bool) _
+  sfT = vec (filter (λ x → T? (snd x)) i&s)
 
-open Constraint
+  -- the scope function
+  sf : Fin (vlength sfT) → Fin nvar
+  sf i = fst (lookup sfT i)
 
-record CSPInstance {ρ : Level} (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
- field
-  ncon : ℕ      -- the number of constraints involved
-  constr : Vec (Constraint {ρ = ρ} nvar dom) ncon
+  ScRestr : (∀ i → Carrier (dom ⟨ i ⟩)) → (∀ j → Carrier(dom ⟨ sf j ⟩))
+  ScRestr f = f ∘ sf
 
- -- f *solves* the instance if it satisfies all constraints.
- isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Type _
- isSolution f = All P constr
-  where
-  P : Pred (Constraint nvar dom) _
-  P c = (satisfies c) f
+  -- point-wise equality of functions
+  _≐_ : Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
+  f ≐ g = ∀ (i : Fin nvar) → (dom ⟨ i ⟩)._≈_ (f i) (g i)
+
+  foldbool : (n : ℕ) (b : Bool) (f : Fin n → Bool) → Bool
+  foldbool zero b f = b
+  foldbool (suc n) b f = foldbool n (b ∧ (f (fromℕ n))) (λ i → f (raise 1 i))
+
+  decide : (f g : (i : Fin nvar) → Carrier (dom ⟨ i ⟩)) → Bool
+  decide f g = foldbool nvar true (λ i → does ((dom ⟨ i ⟩)._≟_ (f i) (g i)))
+
+  ≐-dec : IsDecEquivalence _≐_
+
+  IsDecEquivalence.isEquivalence ≐-dec = record { refl = λ i → (dom ⟨ i ⟩) .refl
+                                                ; sym = λ x i → (dom ⟨ i ⟩) .sym (x i)
+                                                ; trans = λ x y i → (dom ⟨ i ⟩) .trans (x i) (y i) }
 
+  IsDecEquivalence._≟_ ≐-dec = λ x y → decide x y because {!!}
 
-record CSPInstanceList {ρ : Level}
-                       (nvar : ℕ)
-                       (dom : Vec (DecSetoid α ℓ) nvar) : Type (α ⊔ lsuc ρ)  where
- field
-  constr : List (Constraint {ρ = ρ} nvar dom)
+  -- point-wise equality of scope-restricted functions
+  _≐s_ : Rel (∀ i → Carrier (dom ⟨ i ⟩)) ℓ
+  f ≐s g = ∀ j → (dom ⟨ sf j ⟩)._≈_ (f (sf j)) (g (sf j))
 
- -- f *solves* the instance if it satisfies all constraints.
- isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Bool
- isSolution f = all P constr
+ open Constraint
+
+ _satisfies_ : (∀ i → Carrier (dom ⟨ i ⟩)) → Constraint → Type _
+ f satisfies c = Σ[ g ∈ (∀ i → Carrier (dom ⟨ i ⟩)) ]
+                 ( (g ∈ (rel c)) × ((_≐s_ c) f g))
+
+
+ _satisfies?_ : (f : ∀ i → Carrier (dom ⟨ i ⟩)) → (c : Constraint) → Dec (f satisfies c)
+ f satisfies? c = record { does = d ; proof = p }
   where
-  P : (Constraint nvar dom) → Bool
-  P c = does ((satisfies? c) f)
+  d : Bool
+  p : Reflects (f satisfies c) d
+  d = {!!}
+  p = {!!}
+
+
+ record CSPInstance : Type (α ⊔ lsuc ρ)  where
+  field
+   ncon : ℕ      -- the number of constraints involved
+   constr : Vec Constraint ncon
+
+  -- f *solves* the instance if it satisfies all constraints.
+  isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Type _
+  isSolution f = All P constr
+   where
+   P : Pred Constraint _
+   P c = f satisfies c
+
+
+ record CSPInstanceList : Type (α ⊔ lsuc ρ)  where
+  field
+   constr : List Constraint
+
+  -- f *solves* the instance if it satisfies all constraints.
+  isSolution :  (∀ i → Carrier (dom ⟨ i ⟩)) → Bool
+  isSolution f = all P constr
+   where
+   P : Constraint → Bool
+   P c = does (f satisfies? c)
 
 
 \end{code}