From 660a710778a0fc2a9ccc67ec4285bb53ba57b901 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 7 Dec 2022 12:58:45 +0000
Subject: Make more arguments irrelevant.

---
 src/Data/Setoid/Definition.idr         | 20 ++++++++++----------
 src/Data/Setoid/Indexed/Definition.idr |  6 +++---
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/src/Data/Setoid/Definition.idr b/src/Data/Setoid/Definition.idr
index c6bd647..f9d4b85 100644
--- a/src/Data/Setoid/Definition.idr
+++ b/src/Data/Setoid/Definition.idr
@@ -83,14 +83,14 @@ Cast Type Setoid where
   cast a = irrelevantCast a
 
 public export 0
-SetoidHomomorphism : (a,b : Setoid)
-  -> (f : U a -> U b) -> Type
+SetoidHomomorphism : (0  a,b : Setoid)
+  -> (0 f : U a -> U b) -> Type
 SetoidHomomorphism a b f
   = (x,y : U a) -> a.equivalence.relation x y
   -> b.equivalence.relation (f x) (f y)
 
 public export
-record (~>) (A,B : Setoid) where
+record (~>) (0 A,B : Setoid) where
   constructor MkSetoidHomomorphism
   H : U A -> U B
   homomorphic : SetoidHomomorphism A B H
@@ -106,11 +106,11 @@ id a = MkSetoidHomomorphism Prelude.id $ \x, y, prf => prf
 
 ||| Composition of Setoid homomorphisms
 public export
-(.) : {a,b,c : Setoid} -> b ~> c -> a ~> b -> a ~> c
+(.) : b ~> c -> a ~> b -> a ~> c
 g . f = MkSetoidHomomorphism (H g . H f) $ \x,y,prf => g.homomorphic _ _ (f.homomorphic _ _ prf)
 
 public export
-(~~>) : (a,b : Setoid) -> Setoid
+(~~>) : (0 a : Setoid) -> (b : Setoid) -> Setoid
 (~~>) a b = MkSetoid (a ~> b) $
   let 0 relation : (f, g : a ~> b) -> Type
       relation f g = (x : U a) ->
@@ -127,7 +127,7 @@ public export
   }
 
 public export
-post : {a,b,c : Setoid} -> b ~> c -> (a ~~> b) ~> (a ~~> c)
+post : b ~> c -> (a ~~> b) ~> (a ~~> c)
 post h = MkSetoidHomomorphism
   { H = (h .)
   , homomorphic = \f1,f2,prf,x => h.homomorphic _ _ (prf x)
@@ -135,14 +135,14 @@ post h = MkSetoidHomomorphism
 
 ||| Two setoid homomorphism are each other's inverses
 public export
-record Isomorphism {a, b : Setoid} (Fwd : a ~> b) (Bwd : b ~> a) where
+record Isomorphism {0 a, b : Setoid} (Fwd : a ~> b) (Bwd : b ~> a) where
   constructor IsIsomorphism
   BwdFwdId : (a ~~> a).equivalence.relation (Bwd . Fwd) (id a)
   FwdBwdId : (b ~~> b).equivalence.relation (Fwd . Bwd) (id b)
 
 ||| Setoid isomorphism
 public export
-record (<~>) (a, b : Setoid) where
+record (<~>) (0 a, b : Setoid) where
   constructor MkIsomorphism
   Fwd : a ~> b
   Bwd : b ~> a
@@ -161,7 +161,7 @@ sym iso = MkIsomorphism iso.Bwd iso.Fwd (IsIsomorphism iso.Iso.FwdBwdId iso.Iso.
 
 ||| Compose isomorphisms
 public export
-trans : {a,b,c : Setoid} -> (a <~> b) -> (b <~> c) -> (a <~> c)
+trans : {a,c : Setoid} -> (a <~> b) -> (b <~> c) -> (a <~> c)
 trans ab bc = MkIsomorphism (bc.Fwd . ab.Fwd) (ab.Bwd . bc.Bwd) (IsIsomorphism i1 i2)
   where i1 : (x : U a) -> a.equivalence.relation (ab.Bwd.H (bc.Bwd.H (bc.Fwd.H (ab.Fwd.H x)))) x
         i1 x = a.equivalence.transitive _ _ _ (ab.Bwd.homomorphic _ _ (bc.Iso.BwdFwdId _)) (ab.Iso.BwdFwdId x)
@@ -171,7 +171,7 @@ trans ab bc = MkIsomorphism (bc.Fwd . ab.Fwd) (ab.Bwd . bc.Bwd) (IsIsomorphism i
 
 public export
 IsoEquivalence : Equivalence Setoid
-IsoEquivalence = MkEquivalence (<~>) (\_ => refl) (\_,_ => sym) (\_,_,_ => trans)
+IsoEquivalence = MkEquivalence (\a, b => a <~> b) (\_ => refl) (\_,_ => sym) (\_,_,_ => trans)
 
 
 ||| Quotient a type by an function into a setoid
diff --git a/src/Data/Setoid/Indexed/Definition.idr b/src/Data/Setoid/Indexed/Definition.idr
index 59dd497..3eda957 100644
--- a/src/Data/Setoid/Indexed/Definition.idr
+++ b/src/Data/Setoid/Indexed/Definition.idr
@@ -75,12 +75,12 @@ Cast (a -> Type) (IndexedSetoid a) where
   cast b = irrelevantCast b
 
 public export 0
-IndexedSetoidHomomorphism : (x, y : IndexedSetoid a) -> (f : (i : a) -> x.U i -> y.U i) -> Type
+IndexedSetoidHomomorphism : (0 x, y : IndexedSetoid a) -> (0 f : (i : a) -> x.U i -> y.U i) -> Type
 IndexedSetoidHomomorphism x y f = (i : a) -> (a, b : x.U i)
   -> x.equivalence.relation i a b -> (y.equivalence.relation i `on` f i) a b
 
 public export
-record (~>) {0 a : Type} (x, y : IndexedSetoid a) where
+record (~>) {0 a : Type} (0 x, y : IndexedSetoid a) where
   constructor MkIndexedSetoidHomomorphism
   H : (i : a) -> x.U i -> y.U i
   homomorphic : IndexedSetoidHomomorphism x y H
@@ -123,7 +123,7 @@ pwEq : (0 x, y : IndexedSetoid a) -> Rel (x ~> y)
 pwEq x y f g = (i : a) -> (u : x.U i) -> y.equivalence.relation i (f.H i u) (g.H i u)
 
 public export
-(~~>) : (x, y : IndexedSetoid a) -> Setoid
+(~~>) : (0 x : IndexedSetoid a) -> (y : IndexedSetoid a) -> Setoid
 x ~~> y = MkSetoid (x ~> y) $ MkEquivalence
   { relation   = pwEq x y
   , reflexive  = \f, i, u => y.equivalence.reflexive i (f.H i u)
-- 
cgit v1.2.3