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

@@ -82,6 +82,44 @@ module setoid-raw-instances where instance
       }
     }
 
+  -- traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
+  -- traced = record
+  --   { WF = λ {A} {S} {B} f →
+  --     let open Setoid (B × S)
+  --      in ∀ x → ∃₂ λ y z → Func.to f (x , z) ≈ (y , z)
+  --   ; trace = λ {A} {S} {B} f wf → record
+  --     { to = proj₁ ∘ᵈ wf
+  --     -- (eq : x ≈ y) → proj₁ (wf x) ≈ proj₁ (wf y)
+  --     ; cong = λ {x} {y} eq → {!!}
+  --     -- Setoid.reflexive {!!} (≡.cong {!wf!} {!eq!})
+  --       -- let (a₁ , (b₁ , (fx≈a₁ , eq₁))) = wf x
+  --       --     -- (a₁ , (b₁ , f[x×b₁]≈[a₁×b₁])) = wf x
+  --       --     (a₂ , (b₂ , (fy≈a₂ , eq₂))) = wf y
+  --       --     f₁ : A ⟶ B × S
+  --       --     f₁ = f ∘ constʳ (Const.function _ S b₁)
+  --       --     f₂ = f ∘ constʳ (Const.function _ S b₂)
+  --       -- -- a₁ ≈ a₂
+  --       -- in Setoid.trans B (Setoid.sym B fx≈a₁) (Setoid.trans {!!} {!Func.cong f eq!} fy≈a₂)
+  --       -- ⟨ constʳ b₁ ⟩
+  --       -- a₁×b₁
+  --       -- ⟨ sym f[x×b₁]≈[a₁×b₁] ⟩
+  --       -- Func.to f x×b₁
+  --       -- ⟨ ? ⟩
+  --       -- x×b₁
+  --       -- x
+  --       -- ⟨ eq ⟩
+  --       -- y
+  --       -- ⟨ constʳ b₂ ⟩
+  --       -- y×b₂
+  --       -- ⟨ Func.to f y×b₁ ⟩
+  --       -- Func.to f y×b₁
+  --       -- ⟨ f[y×b₂]≈[a₂×b₂] ⟩
+  --       -- a₂×b₂
+  --       -- sym ⟨ constʳ b₂ ⟩
+  --       -- a₂
+  --     }
+  --   }
+
   cartesianClosed :
     ∀ {c ℓ} →
     CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_