From 4c4ca752bcbc900b3ffa30602c955728778dc9a1 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 19 Jul 2025 01:36:42 -0500
Subject: Show equivalence of old and new Hypergraph setoids

---
 Data/Permutation.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'Data/Permutation.agda')

diff --git a/Data/Permutation.agda b/Data/Permutation.agda
index 2413a0d..55c8748 100644
--- a/Data/Permutation.agda
+++ b/Data/Permutation.agda
@@ -2,7 +2,7 @@
 
 open import Level using (Level)
 
-module Data.Permutation {ℓ : Level} (A : Set ℓ) where
+module Data.Permutation {ℓ : Level} {A : Set ℓ} where
 
 import Data.Fin as Fin
 import Data.Fin.Properties as FinProp
@@ -39,8 +39,7 @@ module _ where
 
   -- convert a List permutation to a Vector permutation
   fromList-↭
-      : {A : Set}
-        {xs ys : List A}
+      : {xs ys : List A}
       → xs ↭ ys
       → fromList xs ↭′ fromList ys
   fromList-↭ refl = ↭-refl
-- 
cgit v1.2.3