Some Traced instance for setoid functions

By using categorical operations I don't have to come up with `cong`
proof manually.  It will be composed instead.
I don't know however if this definition is good one, so it'll be
commented out for the time being.

src/Felix/Instances/Setoid/Raw.agda

@@ -2,33 +2,40 @@
 
 module Felix.Instances.Setoid.Raw where
 
-open import Data.Product using (_,_; curry′; uncurry′; ∃₂)
+open import Data.Product using (_,_; _,′_; curry′; 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; _⟶_; cong; _⟨$⟩_) public
+open import Felix.Instances.Setoid.Type
+  using (module setoid-instances; _⟶_; cong; _⟨$⟩_) public
 open setoid-instances public
 
 module setoid-raw-instances where instance
 
+  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
+  equivalent = record
+    { _≈_ = λ {From} {To} f g →
+      let open Setoid To
+      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
+    ; equiv = λ {From} {To} →
+      let open Setoid To
+       in record
+         { refl = λ _ → refl
+         ; sym = λ f≈g x → sym (f≈g x)
+         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
+         }
+    }
+
   category : ∀ {c ℓ} → Category {suc (c ⊔ ℓ)} {c ⊔ ℓ} {obj = Setoid c ℓ} _⟶_
   category = record
     { id = Id.function _
@@ -55,6 +62,16 @@ module setoid-raw-instances where instance
     ; inr = inj₂ₛ
     }
 
+  -- omit until I can be sure it's ok
+  -- traced : ∀ {c ℓ} → Traced {obj = Setoid (c ⊔ ℓ) (c ⊔ ℓ)} _⟶_
+  -- traced = record
+  --   { WF = λ {_} {s} {b} f →
+  --     let open Equivalent equivalent in
+  --     ∃₂ λ (y : ⊤ ⟶ b) (z : ⊤ ⟶ s) →
+  --     f ∘ constʳ z ≈ (y ⦂ z) ∘ !
+  --   ; trace = λ { f (y , z , eq) → exl ∘ f ∘ constʳ z }
+  --   }
+
   cartesianClosed :
     ∀ {c ℓ} →
     CartesianClosed ⦃ products {c ⊔ ℓ} {c ⊔ ℓ} ⦄ ⦃ exponentials {c} {ℓ} ⦄ _⟶_
@@ -72,17 +89,3 @@ module setoid-raw-instances where instance
         Setoid.trans B (f≈g x) (cong g x≈y) }
       }
     }
-
-  equivalent : ∀ {c ℓ} → Equivalent (c ⊔ ℓ) {obj = Setoid c ℓ} _⟶_
-  equivalent = record
-    { _≈_ = λ {From} {To} f g →
-      let open Setoid To
-      in ∀ x → f ⟨$⟩ x ≈ g ⟨$⟩ x
-    ; equiv = λ {From} {To} →
-      let open Setoid To
-       in record
-         { refl = λ _ → refl
-         ; sym = λ f≈g x → sym (f≈g x)
-         ; trans = λ f≈g g≈h x → trans (f≈g x) (g≈h x)
-         }
-    }