diff --git a/UniversalAlgebra/Complexity/FiniteCSP.lagda b/UniversalAlgebra/Complexity/FiniteCSP.lagda
new file mode 100644
index 00000000..b3d9eb8b
--- /dev/null
+++ b/UniversalAlgebra/Complexity/FiniteCSP.lagda
@@ -0,0 +1,254 @@
+n---
+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.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.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 ( ℕ ; zero ; suc )
+open import Function.Base         using ( _∘_ )
+open import Relation.Binary       using ( DecSetoid ; Rel )
+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
+
+\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 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 scope vector,  `s : Vec Bool nvar` , where `s i` is `true` if variable `i` is in the scope
+   of the constraint.
+
+2. a constraint relation, rel, which is a collection of functions mapping
+   variables in the scope to elements of the domain.
+
+\begin{code}
+
+-- syntactic sugar for vector element lookup
+_⟨_⟩ : {A : Set α}{n : ℕ} → Vec A n → Fin n → A
+v ⟨ i ⟩ = (lookup v) i
+
+
+open DecSetoid
+
+-- {nvar : ℕ}{dom : Vec (DecSetoid α ℓ) nvar} → 
+
+open Dec
+
+module finite-csp
+ {ρ : Level}
+ (nvar' : ℕ)
+ (dom : Vec (DecSetoid α ℓ) (suc nvar')) where
+
+ private
+  nvar = suc nvar'
+
+ open Vec≤
+
+ 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
+
+  -- 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
+
+  -- variables in scope along with T in second coordinate
+  sfT : Vec (Fin nvar × Bool) _
+  sfT = vec (filter (λ x → T? (snd x)) i&s)
+
+  -- the scope function
+  sf : Fin (vlength sfT) → Fin nvar
+  sf i = fst (lookup sfT i)
+
+  ScRestr : (∀ i → Carrier (dom ⟨ i ⟩)) → (∀ j → Carrier(dom ⟨ sf j ⟩))
+  ScRestr f = f ∘ sf
+
+  -- 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 {!!}
+
+  -- 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))
+
+ 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
+  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}
+
+
+
+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)
+
diff --git a/UniversalAlgebra/Foundations/Welldefined.lagda b/UniversalAlgebra/Foundations/Welldefined.lagda
index 9fe41266..5e67918a 100644
--- a/UniversalAlgebra/Foundations/Welldefined.lagda
+++ b/UniversalAlgebra/Foundations/Welldefined.lagda
@@ -283,6 +283,7 @@ module _ {A : Type α}{B : Type β} where -- {de : DecidableEquality A} where
  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 ))
@@ -297,6 +298,7 @@ module _ {A : Type α}{B : Type β} where -- {de : DecidableEquality A} where
 
 
 
+
 \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}