diff options
Diffstat (limited to 'src/Data/Setoid/Definition.idr')
| -rw-r--r-- | src/Data/Setoid/Definition.idr | 20 |
1 files changed, 10 insertions, 10 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 |