Struggling with Traced

This is just bunch of commented out code, that I am struggling with.
I can see how this one should hold.  From the well foundedness we can
get `b₁` and `b₂` which bundled with input could be fed to the
function `f` and leter projected away.  However this means that the
sides of `cong` operation are _slightly_ different.

src/Felix/Instances/Setoid/Raw.agda

@@ -2,29 +2,22 @@
 
 module Felix.Instances.Setoid.Raw where
 
-open import Data.Product using (_,_; uncurry′; ∃₂)
+open import Data.Product using (_,_; _,′_; uncurry′; ∃₂; proj₁; proj₂)
 open import Data.Product.Function.NonDependent.Setoid using (<_,_>ₛ; proj₁ₛ; proj₂ₛ)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 open import Data.Sum using ([_,_]; inj₁; inj₂)
 open import Data.Sum.Function.Setoid using ([_,_]ₛ; inj₁ₛ; inj₂ₛ)
-open import Data.Unit.Polymorphic using (tt) renaming (⊤ to ⊤′)
-open import Function using (Congruent; Func; _∘′_) renaming (_∘_ to _∘ᵈ_)
+open import Data.Unit.Polymorphic using (tt)
+open import Function using (Func) renaming (_∘_ to _∘ᵈ_)
 open import Function.Construct.Composition as Comp
 open import Function.Construct.Constant as Const
 open import Function.Construct.Identity as Id
-open import Function.Construct.Setoid as Fun
 open import Level using (_⊔_; suc)
 open import Relation.Binary using (Setoid)
-open import Relation.Binary.PropositionalEquality as ≡ using ()
 
 open import Felix.Equiv using (Equivalent)
 open import Felix.Raw
-  using ( Category; _∘_
-        ; Cartesian; exl; _⊗_; constʳ
-        ; Cocartesian; CartesianClosed; Traced
-        ; ⊤; _×_
-        )
-open import Felix.Instances.Setoid.Type using (module setoid-instances; _⟶_; to; cong; _⟨$⟩_) public
+open import Felix.Instances.Setoid.Type
+  using (module setoid-instances; _⟶_; to; cong; _⟨$⟩_) public
 open setoid-instances public
 
 module setoid-raw-instances where instance
@@ -55,6 +48,25 @@ module setoid-raw-instances where instance
     ; inr = inj₂ₛ
     }
 
+  traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
+  traced {c} {ℓ} = record
+    { WF = λ {a} {s} {b} f →
+      ∀ (x : Carrier a) → ∃₂ λ (y : Carrier b) (z : Carrier s) →
+      let open Setoid (b × s) using (_≈_)
+      in f ⟨$⟩ (x ,′ z) ≈ (y ,′ z)
+    ; trace = λ {a} {s} {b} f wf →
+      -- let init : a ⟶ s
+      --     init = record
+      --       { to = proj₁ ∘ᵈ proj₂ ∘ᵈ wf
+      --       ; cong = λ x≈y → {!!}
+      --       }
+      -- in exl ∘ f ∘ second init ∘ dup
+    record
+      { to = proj₁ ∘ᵈ wf
+      ; cong = λ {x} {y} x≈y → {!!}
+      }
+    } where open Setoid using (Carrier; refl)
+
   cartesianClosed :
     ∀ {c ℓ} →
     CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_