Add code for generating and working with quotients

src/Quotient/Quotient.idr

@@ -0,0 +1,69 @@
+module Quotient
+
+import Control.Isomorphism
+
+%access public export
+%default total
+
+extEq : (a -> b) -> (a -> b) -> Type
+extEq {a} f g = (x : a) -> f x = g x
+
+Rel : Type -> Type
+Rel x = x -> x -> Type
+
+record EqRel (x : Type) where
+  constructor MkEqRel
+  rel : Rel x
+  refl : (a : x) -> rel a a
+  sym : (a, b : x) -> rel a b -> rel b a
+  trans : (a, b, c : x) -> rel a b -> rel b c -> rel a c
+
+parameters (rel : Rel x)
+  data EqClosure' : Rel x where
+    ClosureIncl : rel a b -> EqClosure' a b
+    ClosureRefl : EqClosure' a a
+    ClosureSym : EqClosure' a b -> EqClosure' b a
+    ClosureTrans : EqClosure' a b -> EqClosure' b c -> EqClosure' a c
+
+EqClosure : Rel x -> EqRel x
+EqClosure r = MkEqRel (EqClosure' r)
+                      (\a => ClosureRefl r)
+                      (\a, b, h => ClosureSym r h)
+                      (\a, b, c, h, h' => ClosureTrans r h h')
+
+RespectingMap : (x, y : Type) -> EqRel x -> Type
+RespectingMap x y eq = (f : (x -> y) ** ((a, b : x) -> (rel eq) a b -> f a = f b))
+
+record Quotient (x : Type) (eq : EqRel x) where
+  constructor MkQuotient
+  carrier : Type
+  proj : RespectingMap x carrier eq
+  exists : (y : Type) -> (f : RespectingMap x y eq)
+        -> (g : (carrier -> y) ** (extEq (fst f) (g . (fst proj))))
+  unique : (y : Type) -> (f : RespectingMap x y eq)
+        -> (g : (carrier -> y)) -> extEq (fst f) (g . (fst proj))
+        -> extEq g (fst (exists y f))
+
+Quotient' : (x : Type) -> Rel x -> Type
+Quotient' x eq = Quotient x (EqClosure eq)
+
+existsUnique : (q : Quotient x eq) -> (f : RespectingMap x y eq)
+            -> (g : carrier q -> y) -> (extEq (fst f) (g . (fst $ proj q)))
+            -> (h : carrier q -> y) -> (extEq (fst f) (h . (fst $ proj q)))
+            -> extEq g h
+existsUnique {y=y} (MkQuotient carrier proj exists unique) f g gh h hh x =
+  trans (unique y f g gh x) $ sym $ unique y f h hh x
+
+projectionInducesIdentity : (q : Quotient x eq) -> (f : carrier q -> carrier q) -> extEq (fst $ proj q) (f . (fst $ proj q)) -> extEq f Basics.id
+projectionInducesIdentity q f h x = sym $ existsUnique q (proj q) id (\a => Refl) f h x
+
+QuotientUnique : (q, q' : Quotient x eq)
+              -> (iso : Iso (carrier q) (carrier q') ** (extEq ((to iso) . (fst $ proj q)) (fst $ proj q')))
+QuotientUnique q q' = let
+                        (isoTo ** commTo) = exists q (carrier q') (proj q')
+                        (isoFrom ** commFrom) = exists q' (carrier q) (proj q)
+                        iso = MkIso isoTo isoFrom
+                                (projectionInducesIdentity q' (isoTo . isoFrom) (\a => trans (commTo a) (cong $ commFrom a)))
+                                (projectionInducesIdentity q (isoFrom . isoTo) (\a => trans (commFrom a) (cong $ commTo a)))
+                      in (iso ** (\a => sym $ commTo a))
+

src/Quotient/Quotients.idr

@@ -0,0 +1,24 @@
+module Quotients
+
+import Quotient.Quotient
+
+%access public export
+%default total
+
+trivialEqRel : (x : Type) -> EqRel x
+trivialEqRel x = MkEqRel (\x, y => x = y) (\x => Refl) (\x, y, r => sym r) (\x, y, z, l, r => trans l r)
+
+trivialQuotient : (x : Type) -> Quotient x $ trivialEqRel x
+trivialQuotient x = MkQuotient x
+                      ((id {a=x}) ** (\a, b, h => h))
+                      (\y, f => ((fst f) ** (\a => Refl)))
+                      (\y, f, g, h, a => sym $ h a)
+
+fullEqRel : (x : Type) -> EqRel x
+fullEqRel x = MkEqRel (\x, y => ()) (\x => ()) (\x, y, r => ()) (\x, y, z, l, r => ())
+
+fullQuotient : (x : Type) -> (a : x) -> Quotient x $ fullEqRel x
+fullQuotient x a = MkQuotient ()
+                     ((\b => ()) ** (\a, b, h => Refl))
+                     (\y, f => ((\b => (fst f) a) ** (\b => snd f b a ())))
+                     (\y, f, g, h, () => sym $ h a)

src/Quotient/UnsafeQuotient.idr

@@ -0,0 +1,33 @@
+module UnsafeQuotient
+
+import Quotient.Quotient
+
+%default total
+%access export
+
+private
+data InternalQuotientType : (x : Type) -> (eq : EqRel x) -> Type where
+  InternalWrap : x -> InternalQuotientType x eq
+
+QuotientType : (x : Type) -> (eq : EqRel x) -> Type
+QuotientType = InternalQuotientType
+
+Wrap : x -> QuotientType x eq
+Wrap = InternalWrap
+
+private
+unwrap : QuotientType x eq -> x
+unwrap (InternalWrap a) = a
+
+postulate
+QuotientEquality : (x : Type) -> (eq : EqRel x) -> (rel eq a b) -> Wrap a = Wrap b
+
+UnsafeQuotient : (x : Type) -> (eq : EqRel x) -> Quotient x eq
+UnsafeQuotient x eq = MkQuotient
+                        (QuotientType x eq)
+                        (Wrap ** (\a, b, h => QuotientEquality x eq h))
+                        (\y, f => ((\a => fst f $ unwrap a) ** (\a => Refl)))
+                        (\y, f, g, h, (InternalWrap a) => sym $ h a)
+
+UnsafeQuotient' : (x : Type) -> (eq : Rel x) -> Quotient' x eq
+UnsafeQuotient' x eq = UnsafeQuotient x (EqClosure eq)