WIP: quotients

src/Basic/Category.lidr

@@ -36,7 +36,7 @@ Then, we implement the basic elements a category consists of.
 %
 < record Category where
 %
-A |record| in Idirs is just the product type of several values, which are called the fields of the record. It's a convenient syntax because Idris provides field access and update functions automatically for us. We add also the constructor |MkCategory| to be able to construct concrete values of type |Category|:
+A |record| in Idris is just the product type of several values, which are called the fields of the record. It's a convenient syntax because Idris provides field access and update functions automatically for us. We add also the constructor |MkCategory| to be able to construct concrete values of type |Category|:
 %
 %
 <   constructor MkCategory

src/Monoid/FreeMonoid.lidr

@@ -0,0 +1,35 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Monoid.FreeMonoid
+>
+> import Data.Fin
+> import Interfaces.Verified
+> import Monoid.Monoid
+>
+> %access public export
+> %default total
+>
+> FreeMonoid : Type -> Monoid
+> FreeMonoid t = MkMonoid (List t) %implementation
+>
+> finSetToFreeMonoid : Nat -> Monoid
+> finSetToFreeMonoid n = FreeMonoid (Fin n)

src/MonoidalCategory/FreeQuotients.idr

@@ -0,0 +1,99 @@
+-- \iffalse
+-- SPDX-License-Identifier: AGPL-3.0-only
+
+-- This file is part of `idris-ct` Category Theory in Idris library.
+
+-- Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+-- This program is free software: you can redistribute it and/or modify
+-- it under the terms of the GNU Affero General Public License as published by
+-- the Free Software Foundation, either version 3 of the License, or
+-- (at your option) any later version.
+
+-- This program is distributed in the hope that it will be useful,
+-- but WITHOUT ANY WARRANTY; without even the implied warranty of
+-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-- GNU Affero General Public License for more details.
+
+-- You should have received a copy of the GNU Affero General Public License
+-- along with this program.  If not, see <https://www.gnu.org/licenses/>.
+-- \fi
+
+module MonoidalCategory.FreeQuotients
+
+import Basic.Category
+import Basic.Functor
+import Basic.Isomorphism
+import Basic.NaturalIsomorphism
+import Basic.NaturalTransformation
+import Data.List
+import Monoid.FreeMonoid
+import Monoid.Monoid
+import MonoidalCategory.StrictMonoidalCategory
+import MonoidalCategory.StrictSymmetricMonoidalCategory
+import MonoidalCategory.SymmetricMonoidalCategoryHelpers
+import Product.ProductCategory
+import Quotient.Quotient
+import Quotient.UnsafeQuotient
+
+%access public export
+%default total
+
+parameters (t : Type, generatingMorphisms : List (List t, List t), extra : (List t -> List t -> Type) -> List t -> List t -> Type)
+
+  data PreFreeMorphism : List t -> List t -> Type where
+    MkIdFreeMorphism          : (x : List t) -> PreFreeMorphism x x
+    MkCompositionFreeMorphism : PreFreeMorphism a b
+                             -> PreFreeMorphism b c
+                             -> PreFreeMorphism a c
+    MkGeneratingFreeMorphism  : (e : (List t, List t))
+                             -> Elem e generatingMorphisms
+                             -> PreFreeMorphism (Basics.fst e) (Basics.snd e)
+    MkExtra                   : extra PreFreeMorphism a b -> PreFreeMorphism a b
+
+  data PreFreeMorphismEquality : (domain, codomain : List t) -> Rel (PreFreeMorphism domain codomain) where
+    LeftIdentityEq : (as, bs : List t)
+                  -> (fm : PreFreeMorphism as bs)
+                  -> PreFreeMorphismEquality as bs (MkCompositionFreeMorphism (MkIdFreeMorphism as) fm) fm
+    RightIdentityEq : (as, bs : List t)
+                  -> (fm : PreFreeMorphism as bs)
+                  -> PreFreeMorphismEquality as bs (MkCompositionFreeMorphism fm (MkIdFreeMorphism bs)) fm
+    AssociativeEq : (as, bs, cs, ds : List t)
+                 -> (fm1 : PreFreeMorphism as bs)
+                 -> (fm2 : PreFreeMorphism bs cs)
+                 -> (fm3 : PreFreeMorphism cs ds)
+                 -> PreFreeMorphismEquality as ds
+                                         (MkCompositionFreeMorphism fm1 (MkCompositionFreeMorphism fm2 fm3))
+                                         (MkCompositionFreeMorphism (MkCompositionFreeMorphism fm1 fm2) fm3)
+
+  FreeMorphism : (a, b : List t) -> Quotient' (PreFreeMorphism a b) (PreFreeMorphismEquality a b)
+  FreeMorphism a b = UnsafeQuotient' (PreFreeMorphism a b) (PreFreeMorphismEquality a b)
+
+parameters (t : Type, generatingMorphisms : List (List t, List t))
+
+  data PreFreeMonoidalMorphism : ((List t -> List t -> Type) -> List t -> List t -> Type) -> List t -> List t -> Type where
+    MkMonoidalFromFree          : PreFreeMorphism t generatingMorphisms extra a b -> PreFreeMonoidalMorphism extra a b
+    MkJuxtapositionFreeMorphism : PreFreeMonoidalMorphism extra a b
+                               -> PreFreeMonoidalMorphism extra c d
+                               -> PreFreeMonoidalMorphism extra (a ++ c) (b ++ d)
+    MkExtraMonoidal             : extra (PreFreeMonoidalMorphism extra) a b -> PreFreeMonoidalMorphism extra a b
+
+  IdFreeMonoidalMorphism : (x : List t) -> PreFreeMonoidalMorphism extra x x
+  IdFreeMonoidalMorphism x = MkMonoidalFromFree $ MkIdFreeMorphism _ _ _ x
+
+  data PreFreeMonoidalMorphismEquality : (extra : (List t -> List t -> Type) -> List t -> List t -> Type)
+                                      -> (domain, codomain : List t)
+                                      -> Rel (PreFreeMonoidalMorphism extra domain codomain) where
+    FreeTensorIdEq : (a, b : List t)
+                  -> PreFreeMonoidalMorphismEquality extra (a ++ b) (a ++ b)
+                       (MkJuxtapositionFreeMorphism (IdFreeMonoidalMorphism a) (IdFreeMonoidalMorphism b))
+                       (IdFreeMonoidalMorphism (a ++ b))
+
+-- parameters (t : Type, generatingMorphisms : List (List t, List t), extra : List t -> List t -> Type)
+
+--   data PreFreeSymmetricMonoidalMorphismExtra : List t -> List t -> Type where
+--     MkSymmetryFreeMorphism : (x, y : List t) -> PreFreeSymmetricMonoidalMorphismExtra (x ++ y) (y ++ x)
+--     MkExtraSymmetric       : extra a b -> PreFreeSymmetricMonoidalMorphismExtra a b
+
+--   PreFreeSymmetricMonoidalMorphism : List t -> List t -> Type
+--   PreFreeSymmetricMonoidalMorphism = PreFreeMonoidalMorphism t generatingMorphisms PreFreeSymmetricMonoidalMorphismExtra

src/MonoidalCategory/StrictMonoidalCategory.lidr

@@ -23,8 +23,12 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > import Basic.Category
 > import Basic.Functor
+> import Monoid.Monoid
 > import Product.ProductCategory
 >
+> -- contrib
+> import Interfaces.Verified
+>
 > %access public export
 > %default total
 >
@@ -49,3 +53,8 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                   (mapObj tensor (a,c), e)
 >                                   (mapObj tensor (b,d), f)
 >                                   (MkProductMorphism (mapMor tensor (a,c) (b,d) (MkProductMorphism g h)) k)
+>
+> smcObjectMonoid : StrictMonoidalCategory -> Monoid.Monoid
+> smcObjectMonoid smc = MkMonoid
+>   (obj (cat smc))
+>   ?asdf

src/MonoidalCategory/StrictSymmetricMonoidalCategory.lidr

@@ -0,0 +1,118 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module MonoidalCategory.StrictSymmetricMonoidalCategory
+>
+> import Basic.Category
+> import Basic.Functor
+> import Basic.NaturalIsomorphism
+> import Basic.NaturalTransformation
+> import MonoidalCategory.StrictMonoidalCategory
+> import MonoidalCategory.SymmetricMonoidalCategoryHelpers
+> import Product.ProductCategory
+>
+> %access public export
+> %default total
+>
+> StrictUnitCoherence :
+>      (cat : Category)
+>   -> (unit : obj cat)
+>   -> (symmetry : NaturalIsomorphism (productCategory cat cat)
+>                                     cat
+>                                     tensor
+>                                     (functorComposition (productCategory cat cat)
+>                                                         (productCategory cat cat)
+>                                                         cat
+>                                                         (swapFunctor cat cat)
+>                                                         tensor))
+>   -> (a : obj cat)
+>   -> Type
+> StrictUnitCoherence cat unit symmetry a =
+>   (component (natTrans symmetry) (a, unit)) = identity cat a
+>
+> StrictAssociativityCoherence :
+>      (cat : Category)
+>   -> (tensor : CFunctor (productCategory cat cat) cat)
+>   -> (tensorIsAssociativeObj :
+>           (a, b, c : obj cat)
+>        -> mapObj tensor (a, mapObj tensor (b, c)) = mapObj tensor (mapObj tensor (a, b), c))
+>   -> (symmetry : NaturalIsomorphism (productCategory cat cat)
+>                                     cat
+>                                     tensor
+>                                     (functorComposition (productCategory cat cat)
+>                                                         (productCategory cat cat)
+>                                                         cat
+>                                                         (swapFunctor cat cat)
+>                                                         tensor))
+>   -> (a, b, c : obj cat)
+>   -> Type
+> StrictAssociativityCoherence cat tensor tensorIsAssociativeObj symmetry a b c =
+>   component (natTrans symmetry) (a, mapObj tensor (b, c)) =
+>   compose cat
+>           (mapObj tensor (mapObj tensor (a, b), c))
+>           (mapObj tensor (mapObj tensor (b, a), c))
+>           (mapObj tensor (mapObj tensor (b, c), a))
+>           (mapMor tensor
+>                   (mapObj tensor (a, b), c)
+>                   (mapObj tensor (b, a), c)
+>                   (MkProductMorphism (component (natTrans symmetry) (a, b)) (identity cat c)))
+>           (rewrite sym (tensorIsAssociativeObj b a c) in
+>            rewrite sym (tensorIsAssociativeObj b c a) in (mapMor tensor
+>                                                                  (b, (mapObj tensor (a, c)))
+>                                                                  (b, (mapObj tensor (c, a)))
+>                                                                  (MkProductMorphism (identity cat b)
+>                                                                                     (component (natTrans symmetry)
+>                                                                                                (a, c)))))
+>
+> data StrictSymmetricMonoidalCategory : Type where
+>   MkStrictSymmetricMonoidalCategory :
+>        (smcat : StrictMonoidalCategory)
+>     -> (symmetry : NaturalIsomorphism (productCategory (cat smcat) (cat smcat))
+>                                       (cat smcat)
+>                                       (tensor smcat)
+>                                       (functorComposition (productCategory (cat smcat) (cat smcat))
+>                                                           (productCategory (cat smcat) (cat smcat))
+>                                                           (cat smcat)
+>                                                           (swapFunctor (cat smcat) (cat smcat))
+>                                                           (tensor smcat)))
+>     -> ((a : obj (cat smcat)) -> StrictUnitCoherence (cat smcat) (unit smcat) symmetry a)
+>     -> ((a, b, c : obj (cat smcat)) -> StrictAssociativityCoherence (cat smcat)
+>                                                                     (tensor smcat)
+>                                                                     (tensorIsAssociativeObj smcat)
+>                                                                     symmetry
+>                                                                     a b c)
+>     -> ((a, b : obj (cat smcat)) -> InverseLaw (cat smcat) (tensor smcat) symmetry a b)
+>     -> StrictSymmetricMonoidalCategory
+>
+> smcat : StrictSymmetricMonoidalCategory -> StrictMonoidalCategory
+> smcat (MkStrictSymmetricMonoidalCategory smcat _ _ _ _) = smcat
+>
+> symmetry :
+>      (ssmc : StrictSymmetricMonoidalCategory)
+>   -> NaturalIsomorphism (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                         (cat (smcat ssmc))
+>                         (tensor (smcat ssmc))
+>                         (functorComposition (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (productCategory (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (cat (smcat ssmc))
+>                                             (swapFunctor (cat (smcat ssmc)) (cat (smcat ssmc)))
+>                                             (tensor (smcat ssmc)))
+> symmetry (MkStrictSymmetricMonoidalCategory _ symmetry _ _ _) = symmetry

src/Quotient/Quotient.idr

@@ -0,0 +1,69 @@
+module Quotient.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 Quotient.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)