diff --git a/src/Quotient/Quotient.idr b/src/Quotient/Quotient.idr new file mode 100644 index 0000000..380af72 --- /dev/null +++ b/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)) + diff --git a/src/Quotient/Quotients.idr b/src/Quotient/Quotients.idr new file mode 100644 index 0000000..b47e6d9 --- /dev/null +++ b/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) diff --git a/src/Quotient/UnsafeQuotient.idr b/src/Quotient/UnsafeQuotient.idr new file mode 100644 index 0000000..3288f55 --- /dev/null +++ b/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)