Move dagger for daggerunctors to a where clause

src/Categories/Category/Dagger/Construction/DaggerFunctors.agda

@@ -19,14 +19,22 @@ DaggerFunctors : (C : DaggerCategory o ℓ e) (D : DaggerCategory o′ ℓ′ e
 DaggerFunctors C D = record
   { C = cat.DaggerFunctors C D
   ; hasDagger = record
-    { _† = λ {F} {G} α →
-      let
-         module F = DaggerFunctor F
-         module G = DaggerFunctor G
-         module α = NaturalTransformation α
-      -- We avoid using ntHelper here to preserve α's distinct commute and
-      -- sym-commute in case they have been defined explicitly.
-      in record
+    { _† = λ {F} {G} α → dagger F G α
+    ; †-identity = †-identity
+    ; †-homomorphism = †-homomorphism
+    ; †-resp-≈ = λ α≈β → †-resp-≈ α≈β
+    ; †-involutive = λ α → †-involutive (NaturalTransformation.η α _)
+    }
+  }
+  where
+    open DaggerCategory C using () renaming (_† to _‡)
+    open DaggerCategory D hiding (C)
+    open HomReasoning
+
+    dagger : ∀ (F G : DaggerFunctor C D)
+           → NaturalTransformation (DaggerFunctor.functor F) (DaggerFunctor.functor G)
+           → NaturalTransformation (DaggerFunctor.functor G) (DaggerFunctor.functor F)
+    dagger F G α = record
       { η = λ X → α.η X †
       ; commute = λ {X Y} f → begin
         α.η Y † ∘ G.₁ f       ≈˘⟨ †-involutive _ ⟩
@@ -51,13 +59,7 @@ DaggerFunctors C D = record
         (α.η Y † ∘ G.₁ f) † † ≈⟨ †-involutive _ ⟩
         α.η Y † ∘ G.₁ f       ∎
       }
-    ; †-identity = †-identity
-    ; †-homomorphism = †-homomorphism
-    ; †-resp-≈ = λ α≈β → †-resp-≈ α≈β
-    ; †-involutive = λ α → †-involutive (NaturalTransformation.η α _)
-    }
-  }
-  where
-    open DaggerCategory C using () renaming (_† to _‡)
-    open DaggerCategory D hiding (C)
-    open HomReasoning
+      where
+        module F = DaggerFunctor F
+        module G = DaggerFunctor G
+        module α = NaturalTransformation α