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