summaryrefslogtreecommitdiff
path: root/src/Data/Setoid/Definition.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Setoid/Definition.idr')
-rw-r--r--src/Data/Setoid/Definition.idr193
1 files changed, 193 insertions, 0 deletions
diff --git a/src/Data/Setoid/Definition.idr b/src/Data/Setoid/Definition.idr
new file mode 100644
index 0000000..c6bd647
--- /dev/null
+++ b/src/Data/Setoid/Definition.idr
@@ -0,0 +1,193 @@
+||| Basic definition and notation for setoids
+module Data.Setoid.Definition
+
+import public Control.Relation
+import public Control.Order
+
+import Data.Vect
+import public Data.Fun.Nary
+
+infix 5 ~>, ~~>, <~>
+
+%default total
+
+public export
+record Equivalence (A : Type) where
+ constructor MkEquivalence
+ 0 relation: Rel A
+ reflexive : (x : A) -> relation x x
+ symmetric : (x, y : A) -> relation x y -> relation y x
+ transitive: (x, y, z : A) -> relation x y -> relation y z
+ -> relation x z
+
+public export
+EqualEquivalence : (0 a : Type) -> Equivalence a
+EqualEquivalence a = MkEquivalence
+ { relation = (===)
+ , reflexive = \_ => Refl
+ , symmetric = \_,_, Refl => Refl
+ , transitive = \_,_,_,Refl,Refl => Refl
+ }
+
+public export
+record Setoid where
+ constructor MkSetoid
+ 0 U : Type
+ equivalence : Equivalence U
+
+public export
+record PreorderData A (rel : Rel A) where
+ constructor MkPreorderData
+ reflexive : (x : A) -> rel x x
+ transitive : (x,y,z : A) -> rel x y -> rel y z -> rel x z
+
+public export
+[PreorderWorkaround] (Reflexive ty rel, Transitive ty rel) => Preorder ty rel where
+
+public export
+MkPreorderWorkaround : {preorderData : PreorderData ty rel} -> Order.Preorder ty rel
+MkPreorderWorkaround {preorderData} =
+ let reflexiveArg = MkReflexive {ty, rel} $
+ lam Hidden (\y => rel y y) preorderData.reflexive
+ transitiveArg = MkTransitive {ty} {rel} $
+ Nary.curry 3 Hidden
+ (\[x,y,z] =>
+ x `rel` y ->
+ y `rel` z ->
+ x `rel` z)
+ (\[x,y,z] => preorderData.transitive _ _ _)
+
+ in PreorderWorkaround
+public export
+reflect : (a : Setoid) -> {x, y : U a} -> x = y -> a.equivalence.relation x y
+reflect a Refl = a.equivalence.reflexive _
+
+public export
+MkPreorder : {0 a : Type} -> {0 rel : Rel a}
+ -> (reflexive : (x : a) -> rel x x)
+ -> (transitive : (x,y,z : a) -> rel x y -> rel y z -> rel x z)
+ -> Preorder a rel
+MkPreorder reflexive transitive = MkPreorderWorkaround {preorderData = MkPreorderData reflexive transitive}
+
+public export
+cast : (a : Setoid) -> Preorder (U a) (a.equivalence.relation)
+cast a = MkPreorder a.equivalence.reflexive a.equivalence.transitive
+
+namespace ToSetoid
+ public export
+ irrelevantCast : (0 a : Type) -> Setoid
+ irrelevantCast a = MkSetoid a (EqualEquivalence a)
+
+public export
+Cast Type Setoid where
+ cast a = irrelevantCast a
+
+public export 0
+SetoidHomomorphism : (a,b : Setoid)
+ -> (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
+ constructor MkSetoidHomomorphism
+ H : U A -> U B
+ homomorphic : SetoidHomomorphism A B H
+
+public export
+mate : {b : Setoid} -> (a -> U b) -> (irrelevantCast a ~> b)
+mate f = MkSetoidHomomorphism f $ \x,y, prf => reflect b (cong f prf)
+
+||| Identity Setoid homomorphism
+public export
+id : (a : Setoid) -> a ~> a
+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
+g . f = MkSetoidHomomorphism (H g . H f) $ \x,y,prf => g.homomorphic _ _ (f.homomorphic _ _ prf)
+
+public export
+(~~>) : (a,b : Setoid) -> Setoid
+(~~>) a b = MkSetoid (a ~> b) $
+ let 0 relation : (f, g : a ~> b) -> Type
+ relation f g = (x : U a) ->
+ b.equivalence.relation (f.H x) (g.H x)
+ in MkEquivalence
+ { relation
+ , reflexive = \f,v =>
+ b.equivalence.reflexive (f.H v)
+ , symmetric = \f,g,prf,w =>
+ b.equivalence.symmetric _ _ (prf w)
+ , transitive = \f,g,h,f_eq_g, g_eq_h, q =>
+ b.equivalence.transitive _ _ _
+ (f_eq_g q) (g_eq_h q)
+ }
+
+public export
+post : {a,b,c : Setoid} -> b ~> c -> (a ~~> b) ~> (a ~~> c)
+post h = MkSetoidHomomorphism
+ { H = (h .)
+ , homomorphic = \f1,f2,prf,x => h.homomorphic _ _ (prf x)
+ }
+
+||| Two setoid homomorphism are each other's inverses
+public export
+record Isomorphism {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
+ constructor MkIsomorphism
+ Fwd : a ~> b
+ Bwd : b ~> a
+
+ Iso : Isomorphism Fwd Bwd
+
+||| Identity (isomorphism _)
+public export
+refl : {a : Setoid} -> a <~> a
+refl = MkIsomorphism (id a) (id a) (IsIsomorphism a.equivalence.reflexive a.equivalence.reflexive)
+
+||| Reverse an isomorphism
+public export
+sym : a <~> b -> b <~> a
+sym iso = MkIsomorphism iso.Bwd iso.Fwd (IsIsomorphism iso.Iso.FwdBwdId iso.Iso.BwdFwdId)
+
+||| Compose isomorphisms
+public export
+trans : {a,b,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)
+
+ i2 : (x : U c) -> c.equivalence.relation (bc.Fwd.H (ab.Fwd.H (ab.Bwd.H (bc.Bwd.H x)))) x
+ i2 x = c.equivalence.transitive _ _ _ (bc.Fwd.homomorphic _ _ (ab.Iso.FwdBwdId _)) (bc.Iso.FwdBwdId x)
+
+public export
+IsoEquivalence : Equivalence Setoid
+IsoEquivalence = MkEquivalence (<~>) (\_ => refl) (\_,_ => sym) (\_,_,_ => trans)
+
+
+||| Quotient a type by an function into a setoid
+|||
+||| Instance of the more general coequaliser of two setoid morphisms.
+public export
+Quotient : (b : Setoid) -> (a -> U b) -> Setoid
+Quotient b q = MkSetoid a $
+ let 0 relation : a -> a -> Type
+ relation x y = b.equivalence.relation (q x) (q y)
+ in MkEquivalence
+ { relation = relation
+ , reflexive = \x =>
+ b.equivalence.reflexive (q x)
+ , symmetric = \x,y =>
+ b.equivalence.symmetric (q x) (q y)
+ , transitive = \x,y,z =>
+ b.equivalence.transitive (q x) (q y) (q z)
+ }
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:04:10 +0000