diff --git a/src/Algebra/Group.ard b/src/Algebra/Group.ard
index d1044108..b513bd18 100644
--- a/src/Algebra/Group.ard
+++ b/src/Algebra/Group.ard
@@ -1,7 +1,10 @@
+\import Algebra.Meta
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
+\import Algebra.Pointed
 \import Data.Array
 \import Data.Or
+\import Equiv
 \import Function.Meta ($)
 \import Logic
 \import Meta
@@ -13,9 +16,16 @@
 
 \class Group \extends CancelMonoid {
   | inverse : E -> E
+
   | inverse-left {x : E} : inverse x * x = ide
   | inverse-right {x : E} : x * inverse x = ide
 
+  \default inverse-left => make-inverse-left inverse inverse-right
+  \default inverse-right => make-inverse-left {Monoid.op} inverse inverse-left
+
+  \default ide-left {x} => make-ide-left E (*) ide inverse *-assoc ide-right inverse-right inverse-left x
+  \default ide-right {x} => make-ide-left E (\lam (x y : E) => y * x) ide inverse (\lam {x y z : E} => inv (*-assoc {_} {z} {y} {x})) ide-left inverse-left inverse-right x
+
   | cancel_*-left x {y} {z} p =>
       y                   ==< inv ide-left >==
       ide * y             ==< pmap (`* y) (inv inverse-left) >==
@@ -96,28 +106,49 @@
                 (\new Inv e (inverse e) inverse-left inverse-right)
                 (\new Inv e' (inverse e') inverse-left inverse-right)
     }
-}
-
-\func conjugate {E : Group} (g : E) (h : E) : E => g * h * inverse g
-
-\func conjugate-via-id {E : Group} (g : E) : conjugate E.ide g = g =>
-  conjugate E.ide g ==< idp >==
-  E.ide * g * inverse E.ide ==< E.*-assoc >==
-  E.ide * (g * inverse E.ide) ==< E.ide-left >==
-  g * (inverse E.ide) ==< pmap (g * ) E.inverse_ide >==
-  g * E.ide ==< E.ide-right >==
-  g `qed
-
-\func conjugate-id  {E : Group} (g : E) : conjugate g E.ide = E.ide =>
-  conjugate g E.ide ==< idp >==
-  g * E.ide * (inverse g) ==< pmap (\lam z => z * (inverse g)) E.ide-right >==
-  g * (inverse g) ==< E.inverse-right >==
-  E.ide `qed
-
 
+  \private \lemma make-inverse-left {M : Monoid} (inverse : M -> M) (inverse-right : \Pi {x : M} -> x * inverse x = ide) {x : M} : inverse x * x = ide
+    => \have | inverse-x-idempotent : (inverse x * x) * (inverse x * x) = inverse x * x =>
+                (inverse x * x) * (inverse x * x) ==< *-assoc >==
+                inverse x * (x * (inverse x * x)) ==< pmap (inverse x *) (inv *-assoc) >==
+                inverse x * ((x * inverse x) * x) ==< cong inverse-right >==
+                inverse x * (ide * x)             ==< inv *-assoc >==
+                (inverse x * ide) * x             ==< cong ide-right >==
+                inverse x * x                     `qed
+             | idempotent-is-trivial {a : M} (a-idempotent : a * a = a) : a = ide =>
+                a                   ==< inv ide-right >==
+                a * ide             ==< cong (inv inverse-right) >==
+                a * (a * inverse a) ==< inv *-assoc >==
+                (a * a) * inverse a ==< cong a-idempotent >==
+                a * inverse a       ==< inverse-right >==
+                ide                 `qed
+       \in idempotent-is-trivial inverse-x-idempotent
+
+  -- TODO: Use semigroup
+  \private \lemma make-ide-left (X : \Set) (* : X -> X -> X) (ide : X) (inverse : X -> X)
+                       (*-assoc : \Pi {x y z : X} -> * (* x y) z = * x (* y z))
+                       (ide-right : \Pi {x : X} -> * x ide = x)
+                       (inverse-right : \Pi {x : X} -> * x (inverse x) = ide)
+                       (inverse-left : \Pi {x : X} -> * (inverse x) x = ide)
+                       (x : X) : * ide x = x =>
+    * ide x                ==< pmap (* __ x) (inv inverse-right) >==
+    * (* x (inverse x)) x  ==< *-assoc >==
+    * x (* (inverse x) x)  ==< cong inverse-left >==
+    * x ide                ==< ide-right >==
+    x                      `qed
+
+
+  \func translate-is-Equiv {G : Group} (h : G) : QEquiv (h *) \cowith
+    | ret => inverse h *
+    | ret_f _ => rewrite (inv G.*-assoc, G.inverse-left, G.ide-left) idp
+    | f_sec _ => rewrite (inv G.*-assoc, G.inverse-right, G.ide-left) idp
+}
 
 \func \infixl 7 / {G : Group} (x y : G) => x * inverse y
 
+\func conjugate {E : Group} (g h : E)
+  => g * h * inverse g
+
 \class AddGroup \extends AddMonoid {
   | negative : E -> E
   | negative-left {x : E} : negative x + x = zro
diff --git a/src/Algebra/Group/Aut.ard b/src/Algebra/Group/Aut.ard
index dc9d234b..81713588 100644
--- a/src/Algebra/Group/Aut.ard
+++ b/src/Algebra/Group/Aut.ard
@@ -1,4 +1,6 @@
 \import Algebra.Group
+\import Algebra.Monoid
+\import Category
 \import Paths
 
 \instance Aut {A : \1-Type} (a : A) : Group (a = a)
@@ -9,4 +11,10 @@
   | *-assoc {x} {y} {z} => *>-assoc x y z
   | inverse => inv
   | inverse-left {x} => inv_*> x
-  | inverse-right {x} => *>_inv x
\ No newline at end of file
+
+\func End {C : Precat} (c : C) : Monoid (Hom c c) \cowith
+  | ide => id c
+  | * => ∘
+  | ide-left => id-left
+  | ide-right => id-right
+  | *-assoc => o-assoc
diff --git a/src/Algebra/Group/Category.ard b/src/Algebra/Group/Category.ard
index 37085538..f35e06f7 100644
--- a/src/Algebra/Group/Category.ard
+++ b/src/Algebra/Group/Category.ard
@@ -1,10 +1,11 @@
 \import Algebra.Group
 \import Algebra.Group.Sub
+\import Algebra.Meta
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
 \import Algebra.Pointed
 \import Algebra.Pointed.Category
-\import Category (Cat, Precat)
+\import Category (Cat, Iso)
 \import Category.Functor
 \import Category.Meta
 \import Category.Subcat
@@ -13,6 +14,7 @@
 \import Function.Meta
 \import Logic
 \import Logic.Meta
+\import Meta
 \import Paths
 \import Paths.Meta
 \import Set.Category
@@ -22,6 +24,8 @@
   \override Dom : Group
   \override Cod : Group
 
+  | func-ide => cancel_*-left (func ide) $ inv func-* *> pmap func ide-left *> inv ide-right
+
   \lemma func-inverse {x : Dom} : func (inverse x) = inverse (func x) => check-for-inv $
     func x * func (inverse x)   ==< inv func-* >==
     func (x * inverse x)        ==< pmap func inverse-right >==
@@ -38,13 +42,13 @@
       ide `qed
 
     | isNormal g {h} p =>
-      func (g * h * inverse g)                 ==< func-* >==
-      func (g * h) * (func (inverse g))        ==< pmap (`* (func (inverse g))) func-* >==
-      func g * func h * (func (inverse g))     ==< pmap (\lam z => func g * z * (func (inverse g))) p >==
-      func g * ide * (func (inverse g))        ==< pmap (`* (func (inverse g))) ide-right >==
-      func g * (func (inverse g))              ==< inv func-* >==
-      func (g * inverse g)                     ==< pmap func inverse-right >==
-      func ide                                 ==< func-ide >==
+      func (g * h * inverse g)                ==< func-* >==
+      func (g * h) * func (inverse g)         ==< pmap (`* (func (inverse g))) func-* >==
+      func g * func h * func (inverse g)      ==< pmap (\lam z => func g * z * func (inverse g)) p >==
+      func g * ide * func (inverse g)         ==< pmap (`* (func (inverse g))) ide-right >==
+      func g * func (inverse g)               ==< inv func-* >==
+      func (g * inverse g)                    ==< pmap func inverse-right >==
+      func ide                                ==< func-ide >==
       ide `qed
 
     | contains_* {x} {y} p q =>
@@ -68,17 +72,16 @@
   \lemma Kernel-injectivity-corrolary (p : isInj func) : TrivialKernel =>
     \lam q => p (q *> inv func-ide)
 
-  \func isIsomorphism : \Prop => \Sigma (isInj func) (isSurj func)
+  \func IsIsomorphism : \Prop => \Sigma (isInj func) (isSurj func)
 }
 
-\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
-  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
-  | func-ide => idp
-  | func-* => idp
-
 \instance GroupCat : Cat Group
   | Hom => GroupHom
-  | id => id
+  | id (G : Group) : GroupHom G G \cowith {
+    | func x => x
+    | func-ide => idp
+    | func-* => idp
+  }
   | o {x y z : Group} (g : GroupHom y z) (f : GroupHom x y) => \new GroupHom {
     | func x => g (f x)
     | func-ide => pmap g f.func-ide *> g.func-ide
@@ -89,18 +92,101 @@
   | o-assoc => idp
   | univalence => sip \lam f _ => exts (func-ide {f}, \lam _ _ => func-* {f}, \lam _ => GroupHom.func-inverse {f})
   \where {
-    \func id (M : Group) : GroupHom M M \cowith
-      | func x => x
-      | func-ide => idp
-      | func-* => idp
+    \func ForgetSet : FaithfulFunctor GroupCat SetCat \cowith
+      | F G => G
+      | Func f => f
+      | Func-id => idp
+      | Func-o => idp
+      | isFaithful => \lam p => ext p
+
+    -- TODO: Prove this more generally for algebraic theories?
+    \lemma Iso<->Inj+Surj {G H : Group} (f : GroupHom G H) : Iso {GroupCat} f <-> f.IsIsomorphism
+      => (\lam p => SetIso->Inj+Surj (ForgetSet.Func-iso p),
+          \lam p => \new Iso {
+            | hinv => \new GroupHom {
+              | func => inve p
+              | func-ide => aux (this_iso p) f.func-ide
+              | func-* {x y : H} => rewrite (this_inv_ap p x, this_inv_ap p y,
+                                             inv f.func-*, inv $ inv_this_ap p (inve p x G.* inve p y),
+                                             inv $ this_inv_ap p x, inv $ this_inv_ap p y ) idp
+            }
+            | hinv_f => exts \lam e => inv (inv_this_ap p e)
+            | f_hinv => exts \lam e => inv (this_inv_ap p e)
+          })
+      \where \private {
+      {- | some  set theoretic lemmas -}
+
+        \lemma this_inv_ap (p : f.IsIsomorphism) (h : H) : h = f (inve p h)
+          => inv (path \lam i => (Iso.f_hinv {this_iso p} i) h)
+
+        \lemma inv_this_ap (p : f.IsIsomorphism) (g : G) : g = inve p (f g)
+          => inv (path \lam i => (Iso.hinv_f {this_iso p} i) g)
+
+        \func this_iso (p : f.IsIsomorphism) => Inj+Surj->SetIso f p.1 p.2
+
+        \func inve (p : f.IsIsomorphism) => Iso.hinv {this_iso p}
+
+        \lemma aux {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} {b : B} (p : f.f a = b) : f.hinv b = a
+          => inv $ rewrite (aux' f, p) idp
+
+        \lemma aux' {A B : \Set} (f : Iso {SetCat} {A} {B}) {a : A} : a = f.hinv (f.f a)
+          => inv (path (\lam i => (f.hinv_f i) a))
+
+        \lemma aux'' {A B : \Set} (f : Iso {SetCat} {A} {B}) {b : B} : b = f.f (f.hinv b)
+          => inv (path (\lam i => (f.f_hinv i) b))
+
+        \lemma SetIso->Inj+Surj(f : Iso {SetCat}) : \Sigma (isInj f.f) (isSurj f.f)
+          => (Equiv.isInj {SetIso->Equiv f}, Equiv.isSurj {SetIso->Equiv f})
+
+        \lemma Inj+Surj->SetIso {X Y : \Set} (f : X -> Y) (p : isInj f) (q : isSurj f) : Iso {SetCat} f
+          => Equiv->SetIso (Equiv.fromInjSurj f p q)
+
+        \lemma Equiv->SetIso {X Y : \Set} {f : X -> Y} (eq : Equiv f) : Iso {SetCat} f \cowith
+          | hinv => Equiv.ret {eq}
+          | hinv_f => ext (Equiv.ret_f {eq})
+          | f_hinv => ext (Equiv.f_ret {eq})
+
+        \lemma SetIso->Equiv {X Y : \Set} {f : X -> Y} (p : Iso {SetCat} f) : Equiv f => \new QEquiv {
+          | ret => Iso.hinv {p}
+          | ret_f x => inv (aux' p {x})
+          | f_sec y => inv (aux'' p {y})
+        }
+      }
+
+    \lemma Iso<->TrivialKer+Surj {G H : Group} (f : GroupHom G H)
+      : Iso {GroupCat} f <-> (\Sigma f.TrivialKernel (isSurj f))
+      => <->trans (Iso<->Inj+Surj f) helper
+      \where \private \func helper : (\Sigma (isInj f)(isSurj f)) <-> (\Sigma f.TrivialKernel (isSurj f)) =>
+        (\lam p => (f.Kernel-injectivity-corrolary p.1, p.2),
+         \lam p => (f.Kernel-injectivity-test p.1, p.2))
   }
 
+\func quotient-map {S : Group} {H : NormalSubGroup S} : GroupHom S H.quotient \cowith
+  | func (s : S) => NormalSubGroup.quotient-proj-setwise s
+  | func-ide => idp
+  | func-* => idp
+
 \instance ImageGroup (f : GroupHom) : Group
   | Monoid => ImageMonoid f
   | inverse a => (inverse a.1, TruncP.map a.2 \lam s => (inverse s.1, f.func-inverse *> pmap inverse s.2))
   | inverse-left => ext inverse-left
   | inverse-right => ext inverse-right
 
+\func ImageGroupLeftHom (f : GroupHom) : GroupHom f.Dom (ImageGroup f) \cowith
+  | MonoidHom => ImageMonoidLeftHom f
+
+\func ImageGroupRightHom (f : GroupHom) : GroupHom (ImageGroup f) f.Cod \cowith
+  | MonoidHom => ImageMonoidRightHom f
+
+\func ImageSubGroup (f : GroupHom) : SubGroup f.Cod \cowith
+  | contains h => ∃(g : f.Dom)(f g = h)
+  | contains_ide => inP (Group.ide {f.Dom}, f.func-ide)
+  | contains_* cont1 cont2 => \case \elim  cont1, \elim  cont2 \with {
+    | inP a, inP b => inP(a.1 * b.1, rewrite (f.func-*, a.2, b.2) idp)
+  }
+  | contains_inverse cont1 => \case \elim cont1 \with {
+    | inP a => inP (inverse a.1, rewrite (f.func-inverse, a.2) idp)
+  }
 
 \record AddGroupHom \extends AddMonoidHom {
   \override Dom : AddGroup
@@ -191,12 +277,27 @@
   | negative-left => ext negative-left
   | negative-right => ext negative-right
 
-\func ImageGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
-  | AddMonoidHom => ImageMonoidLeftHom f
+\func ImageAddGroupLeftHom (f : AddGroupHom) : AddGroupHom f.Dom (ImageAddGroup f) \cowith
+  | AddMonoidHom => ImageAddMonoidLeftHom f
 
-\func ImageGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
-  | AddMonoidHom => ImageMonoidRightHom f
+\func ImageAddGroupRightHom (f : AddGroupHom) : AddGroupHom (ImageAddGroup f) f.Cod \cowith
+  | AddMonoidHom => ImageAddMonoidRightHom f
 
 \instance ImageAbGroup {A : AddGroup} {B : AbGroup} (f : AddGroupHom A B) : AbGroup
   | AddGroup => ImageAddGroup f
-  | AbMonoid => ImageAbMonoid f
\ No newline at end of file
+  | AbMonoid => ImageAbMonoid f
+
+\func conjugateHom {E : Group} (g : E) : GroupHom E E \cowith
+  | func => conjugate g
+  | func-ide => unfold conjugate $ rewrite (E.ide-right, E.inverse-right) idp
+  | func-* {x y : E} =>
+    \have aux {x y z w t e : E} : x * y * z * (w * t * e) = (x * y) * (z * w) * (t * e) => equation
+    \in inv $ rewrite (aux, E.inverse-left, E.ide-right) equation
+
+\lemma conjugate-via-id {G : Group} {g : G} : conjugate ide g = g =>
+  conjugate ide g ==< idp >==
+  ide * g * inverse ide ==< *-assoc >==
+  ide * (g * inverse ide) ==< ide-left >==
+  g * inverse ide ==< pmap (g *) inverse_ide >==
+  g * ide ==< ide-right >==
+  g `qed
\ No newline at end of file
diff --git a/src/Algebra/Group/GSet.ard b/src/Algebra/Group/GSet.ard
index 06e98c17..0349a956 100644
--- a/src/Algebra/Group/GSet.ard
+++ b/src/Algebra/Group/GSet.ard
@@ -1,23 +1,15 @@
 \import Algebra.Group
 \import Algebra.Group.Sub
-\import Algebra.Meta
 \import Algebra.Monoid
-\import Algebra.Monoid.Sub
 \import Algebra.Pointed
-\import Equiv
-\import Function
-\import Function.Meta ($)
 \import Logic
 \import Logic.Meta
 \import Paths
-\import Paths.Meta
 \import Relation.Equivalence
 \import Set
-\import Algebra.Monoid
-\import Set.Category
 
 \class GroupAction (G : Group) \extends BaseSet {
-  | \infixl 8 ** : G -> E -> E -- priority should be bigger than that of "+" in LModule (=7)
+  | \infixl 8 ** : G -> E -> E -- priority should be bigger than priority of "+" in LModule (=7)
   | **-assoc {m n : G} {e : E} : m ** (n ** e) = (m * n) ** e
   | id-action {e : E} : ide ** e = e
 
@@ -81,17 +73,3 @@
                               in~ a1 `qed
                            )
    }
-
--- action by conjugating its own elements
-\func conjAction (G : Group) : GroupAction G \cowith
-  | E => G
-  | ** (g : G)  => conjugate g
-  | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e =>
-  conjugate m (conjugate n e) ==< pmap (conjugate m) idp >==
-  conjugate m (n * e * inverse n ) ==< idp >==
-  m * (n * e * inverse n ) * inverse m ==< lemma-par >==
-  (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >==
-  (m * n) * e * (inverse (m * n)) ==< idp >==
-  conjugate (m * n) e `qed
-  | id-action {e : G} : conjugate ide e = e => conjugate-via-id e
-  \where \lemma lemma-par {a b c d e : G} : a * (b * c * d) * e = (a * b) * c * (d * e) => equation
diff --git a/src/Algebra/Group/GSet/CategoricalDefinition.ard b/src/Algebra/Group/GSet/CategoricalDefinition.ard
new file mode 100644
index 00000000..b977e555
--- /dev/null
+++ b/src/Algebra/Group/GSet/CategoricalDefinition.ard
@@ -0,0 +1,43 @@
+\import Algebra.Group.Aut
+\import Algebra.Monoid
+\import Algebra.Monoid.Category
+\import Category
+\import Category.Functor
+\import Equiv (Equiv)
+\import Paths.Meta
+
+-- TODO: when limits in presheaves are added, write that category of actions is bicomplete whenever the underlying category is bicomplete
+
+\class MonoidCatAction {C : Precat} (M : Monoid) (\classifying  c : C){
+  | act : MonoidHom M (End c)
+
+  \func functor : Functor (DeloopM M) C \cowith
+    | F => \lam _ => c
+    | Func (f : M) => act f
+    | Func-id => act.func-ide
+    | Func-o => act.func-*
+}
+
+\instance DeloopM (M : Monoid) : Precat
+  | Ob => \Sigma
+  | Hom _ _ => M
+  | id _ => M.ide
+  | o => *
+  | id-left => ide-left
+  | id-right => ide-right
+  | o-assoc => *-assoc
+
+\func functor->action {C : Precat} {M : Monoid} (f : Functor (DeloopM M) C) : MonoidCatAction M \cowith
+  | c => f ()
+  | act => \new MonoidHom {
+    | func => Func
+    | func-ide => Func-id
+    | func-* => Func-o
+  }
+
+\func Action<->Functor {C : Precat} {M : Monoid} : Equiv {MonoidCatAction M} {Functor (DeloopM M) C} \cowith
+  | f (c : MonoidCatAction) => c.functor
+  | ret => functor->action
+  | ret_f c => ext (idp, idp)
+  | sec => functor->action
+  | f_sec f => idp
diff --git a/src/Algebra/Group/GSet/Category.ard b/src/Algebra/Group/GSet/Category.ard
index 7da26103..f5d36d97 100644
--- a/src/Algebra/Group/GSet/Category.ard
+++ b/src/Algebra/Group/GSet/Category.ard
@@ -1,37 +1,33 @@
 \import Algebra.Group
 \import Algebra.Group.GSet
-\import Algebra.Group.Sub
 \import Category
 \import Category.Meta
 \import Function (isInj, isSurj)
-\import Function.Meta ($)
 \import Paths
 \import Paths.Meta
-\import Relation.Equivalence
-\import Set
 \import Set.Category
 
-\record EquivariantMap (G : Group) \extends SetHom{
+\record EquivariantMap (G : Group) \extends SetHom {
   \override Dom : GroupAction G
   \override Cod : GroupAction G
   | func-** {e : Dom} {g : G} : func (g ** e) = g ** func e -- equivariance
 
-  \func isIso => \Sigma (isSurj func) (isInj func)
+  \func IsIso => \Sigma (isSurj func) (isInj func)
 }
 
-\func id-equivar {G : Group} (X : GroupAction G) : EquivariantMap G { | Dom => X | Cod => X} \cowith
+\func id-equivar {G : Group} (X : GroupAction G) : EquivariantMap G X X \cowith
   | func (x : X) => x
   | func-** {x : X} {g : G} => idp
 
 \instance GSet (G : Group) : Cat (GroupAction G)
-  | Hom A B => EquivariantMap G { | Dom => A | Cod => B}
+  | Hom A B => EquivariantMap G A B
   | id X => id-equivar X
   | o {x y z : GroupAction G} (g : EquivariantMap G y z) (f : EquivariantMap G x y) => \new EquivariantMap G {
     | func (a : x) => g (f a)
     | func-** {a : x} {h : G} =>
       g ( f (h ** a)) ==< pmap g func-** >==
       g (h ** f a) ==< func-** >==
-      h ** (g (f a)) `qed
+      h ** g (f a) `qed
   }
   | id-left => idp
   | id-right => idp
diff --git a/src/Algebra/Group/GSet/ExampleActions.ard b/src/Algebra/Group/GSet/ExampleActions.ard
new file mode 100644
index 00000000..947bc89e
--- /dev/null
+++ b/src/Algebra/Group/GSet/ExampleActions.ard
@@ -0,0 +1,44 @@
+\import Algebra.Group
+\import Algebra.Group.Category
+\import Algebra.Group.GSet
+\import Algebra.Meta
+\import Algebra.Monoid
+\import Logic
+\import Paths
+\import Paths.Meta
+\import Set
+
+\func TranslationAction (G : Group) : TransitiveGroupAction G \cowith
+  | E => G
+  | ** => G.*
+  | **-assoc => inv G.*-assoc
+  | id-action => G.ide-left
+  | trans => \lam (v v' : G) => inP (v' G.* inverse v, rewrite (G.*-assoc, G.inverse-left) G.ide-right)
+
+\func TranslationActionOnSubsets (G : Group) : GroupAction G \cowith
+  | E => SubSet G
+  | ** (g : G) (p : SubSet G) => \new SubSet G {| contains h => p.contains (inverse g G.* h)}
+  | **-assoc {_ : G} {_ : G} {_ : SubSet G} => ext (ext (\lam (_ : G) => rewrite (inv G.*-assoc, inv G.inverse_*) idp))
+  | id-action => exts (\lam (e1 : G) => rewrite (G.inverse_ide, G.ide-left) idp)
+
+-- action by conjugating its own elements
+\func conjAction (G : Group) : GroupAction G \cowith
+  | E => G
+  | ** (g : G)  => conjugate g
+  | **-assoc {m : G} {n : G} {e : G} : conjugate m (conjugate n e) = conjugate (m * n) e =>
+      conjugate m (conjugate n e) ==< pmap (conjugate m) idp >==
+      conjugate m (n * e * inverse n ) ==< idp >==
+      m * (n * e * inverse n ) * inverse m ==< equation >==
+      (m * n) * e * (inverse n * inverse m) ==< pmap ((m * n * e) *) (inv G.inverse_*) >==
+      (m * n) * e * inverse (m * n) ==< idp >==
+      conjugate (m * n) e `qed
+  | id-action {e : G} : conjugate G.ide e = e => conjugate-via-id
+
+\func trivialAction (G : Group) (E : BaseSet) : GroupAction G E \cowith
+  | ** _ e => e
+  | **-assoc => idp
+  | id-action => idp
+
+\func conjugate-subset {G : Group} (g : G) (S : SubSet G) : SubSet G \cowith
+  | contains h => S.contains (conjugate (inverse g) h)
+
diff --git a/src/Algebra/Group/Lagrange.ard b/src/Algebra/Group/Lagrange.ard
index efbc8d2a..d400e029 100644
--- a/src/Algebra/Group/Lagrange.ard
+++ b/src/Algebra/Group/Lagrange.ard
@@ -3,7 +3,6 @@
 \import Algebra.Monoid
 \import Arith.Nat
 \import Equiv
-\import Equiv.Univalence
 \import Function.Meta
 \import Logic
 \import Logic.Classical
diff --git a/src/Algebra/Group/QuotientProperties.ard b/src/Algebra/Group/QuotientProperties.ard
index 5e95fc32..316c49db 100644
--- a/src/Algebra/Group/QuotientProperties.ard
+++ b/src/Algebra/Group/QuotientProperties.ard
@@ -1,25 +1,19 @@
 \import Algebra.Group
+\import Algebra.Group.Category
 \import Algebra.Group.Sub
 \import Algebra.Monoid
 \import Algebra.Monoid.Category
 \import Algebra.Pointed
 \import Algebra.Pointed.Category
-\import Category (Cat, Precat)
-\import Category.Functor
-\import Category.Meta
-\import Category.Subcat
-\import Equiv
-\import Function
-\import Function.Meta
+\import Category
+\import Function \hiding (id, o)
 \import Logic
 \import Logic.Meta
 \import Paths
 \import Paths.Meta
 \import Relation.Equivalence
 \import Set.Category
-\import Algebra.Group.Category
 \open Group
-\open Algebra.Group.Sub
 
 \func \infix 7 // (G : Group) (H : NormalSubGroup G) : Group => H.quotient
 
@@ -47,13 +41,13 @@
    - $$G \xrightarrow{\pi} G/N \xrightarrow{\text{this\,  function}} H $$ -}
   \func universalQuotientMorphismSetwise (a : N.quotient) : H \elim a
     | in~ n => f n
-    | ~-equiv y x r => equality-check (inverse (f y) * (f x) ==< pmap (\lam y => y * (f x)) (inv f.func-inverse) >==
-    f (inverse y) * (f x) ==< inv func-* >==
+    | ~-equiv y x r => equality-check (inverse (f y) * f x ==< pmap (\lam y => y * f x) (inv f.func-inverse) >==
+    f (inverse y) * f x ==< inv func-* >==
     f (inverse y * x) ==< lemma' f N p r >== ide `qed)
     \where
       \lemma lemma' {x y : G} (f : GroupHom G H) (N : NormalSubGroup G) (p : N SubGroupPreorder.<= f.Kernel)
-                    (r : N.contains ((inverse y) * x)) : f (inverse y * x) = ide =>
-        f (inverse y * x) ==< p ((inverse y) * x) r >== ide `qed
+                    (r : N.contains (inverse y * x)) : f (inverse y * x) = ide =>
+        f (inverse y * x) ==< p (inverse y * x) r >== ide `qed
 
 
   {- | this a synonym for universalQuotientMorphismSetwise used because it is shorter-}
@@ -62,13 +56,13 @@
 
   {- | this is a proof that in the previous assumptions the function
    - universalQuotientMorphismSetwise is multiplicative -}
-  \lemma universalQuotientMorphismMultiplicative (x y : N.quotient) : uqms (x N.quotient.* y) = (uqms x) * (uqms y) \elim x, y
-    | in~ a, in~ a1 => uqms  ((in~ a) N.quotient.* (in~ a1)) ==< idp >==
+  \lemma universalQuotientMorphismMultiplicative (x y : N.quotient) : uqms (x N.quotient.* y) = uqms x * uqms y \elim x, y
+    | in~ a, in~ a1 => uqms  (in~ a N.quotient.* in~ a1) ==< idp >==
                     uqms (in~ (a * a1)) ==< idp >==
                     f (a * a1) ==< f.func-* >==
-                    (f a) * (f a1) ==< pmap ((f a)*) idp >==
-                    (f a) * uqms  (in~ a1) ==< pmap (\lam x => x * uqms (in~ a1)) idp >==
-                   (uqms  (in~ a)) * (uqms (in~ a1)) `qed
+                    f a * f a1 ==< pmap (f a *) idp >==
+                    f a * uqms  (in~ a1) ==< pmap (\lam x => x * uqms (in~ a1)) idp >==
+                   uqms  (in~ a) * uqms (in~ a1) `qed
 
 
   {- | this is a function which gives the homomorphism in the universal property
@@ -142,5 +136,29 @@
   \lemma univKer-epi (p : isSurj f): isSurj univ
     => Triangle.surjectivity-2-out-3 p f.Kernel.quotIsSurj
 
-  \lemma FirstIsoTheorem (p : isSurj f) : univ.isIsomorphism => (univKer-mono, univKer-epi p)
-}
\ No newline at end of file
+  \lemma FirstIsoTheorem (p : isSurj f) : univ.IsIsomorphism => (univKer-mono, univKer-epi p)
+}
+
+-- application of first Isomorphism theorem without need to define local instances
+\func GroupFirstIsoCorollary-setwise{G H : Group} {N : NormalSubGroup G} (f : GroupHom G H) (p : N = f.Kernel) (q : isSurj f):
+  \Sigma(h : GroupHom (G // N) H) h.IsIsomorphism =>
+  transport {NormalSubGroup G} (\lam X => \Sigma (f : GroupHom (G // X) H)f.IsIsomorphism) (inv p) (GroupFirstIsoCorollary-24 f q)
+    \where{
+
+      \func GroupFirstIsoCorollary-2 {G H : Group}(f : GroupHom G H) :
+        GroupHom (G // f.Kernel) H => FirstIsomorphismTheorem.univ {\new FirstIsomorphismTheorem {| G => G | H => H | f => f}}
+
+      \func GroupFirstIsoCorollary-24 {G H : Group}(f : GroupHom G H)(q : isSurj f) :
+        \Sigma (a : GroupHom (G // f.Kernel) H) a.IsIsomorphism => (GroupFirstIsoCorollary-2 f,
+                                                                    FirstIsomorphismTheorem.FirstIsoTheorem {\new FirstIsomorphismTheorem {| G => G | H => H | f => f}} q)
+
+
+      \func GroupFirstIsoCorollary-3 {G H : Group} {N : NormalSubGroup G} (f : GroupHom G H) (p : N = f.Kernel) :
+        GroupHom (G // N) H => transport {NormalSubGroup G} (\lam X => GroupHom (G // X) H) (inv p) (GroupFirstIsoCorollary-2 f)
+
+    }
+
+\func GroupFirstIsoCorollary{G H : Group} {N : NormalSubGroup G} (f : GroupHom G H) (p : N = f.Kernel) (q : isSurj f):
+  \Sigma (f : GroupHom (G // N) H) (Iso {GroupCat} {G // N} {H} f) => ((GroupFirstIsoCorollary-setwise f p q).1,
+                                                                       (GroupCat.Iso<->Inj+Surj (GroupFirstIsoCorollary-setwise f p q).1).2
+                                                                      (GroupFirstIsoCorollary-setwise f p q).2)
diff --git a/src/Algebra/Group/Representation.ard b/src/Algebra/Group/Representation.ard
new file mode 100644
index 00000000..7ce1161a
--- /dev/null
+++ b/src/Algebra/Group/Representation.ard
@@ -0,0 +1,39 @@
+\import Algebra.Group
+\import Algebra.Group.GSet.ExampleActions
+\import Algebra.Group.GSet
+\import Algebra.Module
+\import Algebra.Module.Category
+\import Algebra.Module.LinearMap
+\import Algebra.Pointed
+\import Algebra.Ring
+\import Meta
+\import Paths
+\import Paths.Meta
+
+-- basic reference right now is https://www.uni-math.gwdg.de/tammo/rep.pdf
+-- REPRESENTATION THEORY Tammo tom Dieck
+-- also : https://www.maths.dur.ac.uk/users/jack.g.shotton/repthy/index.html
+
+\class LinRepres \extends LModule, GroupAction {
+  | **-ldistr {g :  G} {e e' : E} : g ** (e + e') = g ** e + g ** e'
+  | **-*c {g :  G} {e : E} {c : R} : g ** (c *c e) = c *c (g ** e)
+
+  \func g**-zro {g : G} : g ** 0 = 0 => rewrite (inv *c_zro-right, **-*c, *c_zro-left, *c_zro-left) idp
+
+  \func g**-negative {g : G} {e : E} : g ** negative e = negative (g ** e) => rewrite (inv neg_ide_*c, **-*c, neg_ide_*c) idp
+
+  \func toLinearMap(g : G) : LinearMap \this \this \cowith
+    | func e => g ** e
+    | func-+ => **-ldistr
+    | func-*c => **-*c
+
+  \func toLinearMap-ide : toLinearMap ide = Ring.ide {LinearMapRing \this} => exts \lam _ => unfold id-action
+}
+
+\func LRepres (R : Ring)(G : Group) : \Type => LinRepres {| R => R | G => G}
+
+\func TrivialAction {R : Ring}(E : LModule R)(G : Group) : LRepres R G \cowith
+  | LModule => E
+  | GroupAction => trivialAction G E
+  | **-*c => idp
+  | **-ldistr => idp
diff --git a/src/Algebra/Group/Representation/Category.ard b/src/Algebra/Group/Representation/Category.ard
new file mode 100644
index 00000000..e19585cb
--- /dev/null
+++ b/src/Algebra/Group/Representation/Category.ard
@@ -0,0 +1,118 @@
+\import Algebra.Group
+\import Algebra.Group.GSet.Category
+\import Algebra.Group.GSet
+\import Algebra.Group.Representation
+\import Algebra.Module
+\import Algebra.Module.Category
+\import Algebra.Module.LinearMap
+\import Algebra.Ring
+\import Category
+\import Category.Meta
+\import Logic
+\import Meta
+\import Paths
+\import Paths.Meta
+
+\record InterwiningMap  {G : Group}  \extends LinearMap {
+  \override Dom : LRepres LinearMap.R G
+  \override Cod : LRepres LinearMap.R G
+  | func-** {e : Dom} {g : G} : func (g ** e) = g ** func e -- equivariance
+  }
+
+\instance RepresentationCat(R : Ring)(G : Group) : Cat (LRepres R G)
+  | Hom => InterwiningMap
+  | id => id-interwining
+  | o {X Y Z : LRepres R G} (f : InterwiningMap Y Z) (g : InterwiningMap X Y) => \new InterwiningMap {
+    | LinearMap => Cat.o {LModuleCat R} f g
+    | func-** =>  rewrite (g.func-**, f.func-**) idp
+  }
+  | id-left => ext idp
+  | id-right => ext idp
+  | o-assoc => ext idp
+  | univalence => sip (\lam (e : InterwiningMap) _ => exts (e.func-zro, \lam _ _ => e.func-+,
+                                                            \lam _ => e.func-negative, \lam _ _ => e.func-*c,
+                                                            \lam _ _ => e.func-** ))
+  \where {
+    \func id-interwining (X : LRepres R G) : InterwiningMap X X \cowith
+      | LinearMap => Cat.id {LModuleCat R} X
+      | func-** => idp
+  }
+
+\func repr+module-iso=>repr-iso {R : Ring} {G : Group}
+                                {A B : LRepres R G} {f : InterwiningMap A B}
+                                (p : Iso {LModuleCat R} f) : Iso f \cowith
+  | hinv => inverseMap {R} {G}{A}{B}{f}{p}
+    | hinv_f => unfold (ext (unfold (exts \lam _ => aux-2)))
+    | f_hinv => unfold (ext (unfold (exts \lam _ => aux)))
+    \where{
+      \func inverseMap => \new InterwiningMap B A {
+        | LinearMap => p.hinv
+        | func-** {b : B} {_ : G} => rewrite (inv (aux {R} {G} {A} {B} {f} {p}{b}),
+                                              inv f.func-**, aux-2, aux) idp
+      }
+      \func aux {b : B} : f (p.hinv b) = b => path (\lam i => (p.f_hinv i) b)
+      \func aux-2 {a : A} : p.hinv (f a) = a => path (\lam i => (p.hinv_f i) a)
+    }
+
+\func KerLRepres {R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : LRepres R G \cowith
+  | LModule => KerLModule f
+  | ** (g : G) (e : KerLModule f) => (g A.** e.1, rewrite (f.func-**, e.2, B.g**-zro) idp)
+  | **-assoc {_ _ : G} {_ : KerLModule f} => exts A.**-assoc
+  | id-action => exts A.id-action
+  | **-ldistr => exts A.**-ldistr
+  | **-*c => exts A.**-*c
+
+
+\func KerLRepresHom {R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : InterwiningMap (KerLRepres f) A \cowith
+  | LinearMap => KerLModuleHom f
+  | func-** => idp
+
+\func ImageLRepres {R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : LRepres R G \cowith
+  | LModule => ImageLModule f
+  | ** (g : G) (e : ImageLModule f) => (g B.** e.1, TruncP.map e.2 \lam s => (g A.** s.1, func-** *> pmap (g B.**) s.2))
+  | **-assoc => ext B.**-assoc
+  | id-action => ext B.id-action
+  | **-ldistr => ext B.**-ldistr
+  | **-*c => ext B.**-*c
+
+
+
+\func ImageLRepresRightHom{R : Ring} {G : Group} (f : InterwiningMap {| R => R | G => G}) : InterwiningMap (ImageLRepres f) f.Cod \cowith
+  | LinearMap => ImageLModuleRightHom f
+  | func-** => idp
+
+
+\func ImageLRepresLeftHom{R : Ring}{G : Group}(f : InterwiningMap {| R => R | G => G}) : InterwiningMap f.Dom (ImageLRepres f) \cowith
+  | LinearMap => ImageLModuleLeftHom f
+  | func-** {_} {_} => exts (rewrite f.func-** idp)
+
+\instance InterwiningMapLModule{R : CRing}{G : Group} (A B : LRepres R G) : LModule R (InterwiningMap A B) \cowith
+  | zro => zeroInterwining
+  | + => addInterwining
+  | zro-left => exts (\lam _ => B.zro-left)
+  | zro-right => exts (\lam _ => B.zro-right)
+  | +-assoc => exts (\lam _ => B.+-assoc)
+  | negative => negativeInterwining
+  | negative-left => exts (\lam _ => B.negative-left)
+  | +-comm => exts (\lam _ => B.+-comm)
+  | *c => mulconstInterwining
+  | *c-assoc => exts (\lam _ => B.*c-assoc)
+  | *c-ldistr => exts (\lam _ => B.*c-ldistr)
+  | *c-rdistr => exts (\lam _ => B.*c-rdistr)
+  | ide_*c => exts (\lam _ => B.ide_*c)
+  \where {
+    \func zeroInterwining : InterwiningMap A B \cowith
+      | LinearMap => LModulePreAdditive.zeroMap
+      | func-** => inv B.g**-zro
+    \func addInterwining (f g : InterwiningMap A B) : InterwiningMap A B \cowith
+      | LinearMap => LModulePreAdditive.addMaps f g
+      | func-** => unfold (rewrite (f.func-**, g.func-**, B.**-ldistr) idp)
+
+    \func negativeInterwining (f : InterwiningMap A B) : InterwiningMap A B \cowith
+      | LinearMap => LModulePreAdditive.negativeMap f
+      | func-** => unfold (rewrite (f.func-**, B.g**-negative) idp)
+
+    \func mulconstInterwining(c : R)(f : InterwiningMap A B) : InterwiningMap A B \cowith
+      | LinearMap => LModule.*c {LinearMapLModule A B} c f
+      | func-** => rewrite (B.**-*c, inv f.func-**) idp
+  }
diff --git a/src/Algebra/Group/Representation/Characters.ard b/src/Algebra/Group/Representation/Characters.ard
new file mode 100644
index 00000000..a589824d
--- /dev/null
+++ b/src/Algebra/Group/Representation/Characters.ard
@@ -0,0 +1,19 @@
+\import Algebra.Group
+\import Algebra.Group.Representation
+\import Algebra.Linear.Matrix
+\import Algebra.Module.LinearMap
+\import Algebra.Module.Trace
+\import Algebra.Ring
+\import Meta
+\import Paths.Meta
+
+\func Character {R : Ring}{G : Group}(E : LRepres R G)
+                {lv : Array E} (bv : E.IsBasis lv)
+                (g : G) : R => Trace (LinearMap.toMatrix lv bv (E.toLinearMap g))
+    \where {
+      \protected \func chi (g : G) : R => Character E bv g
+
+      \func of-1 : chi G.ide = R.natCoef lv.len => unfold chi (unfold Character (rewrite (Matrix-of-1, Trace-ide) idp))
+
+      \func Matrix-of-1 : LinearMap.toMatrix lv bv (E.toLinearMap G.ide) = MatrixRing.ide => rewrite (E.toLinearMap-ide, LinearMap.toMatrix_ide) idp
+    }
\ No newline at end of file
diff --git a/src/Algebra/Group/Representation/Irreducible.ard b/src/Algebra/Group/Representation/Irreducible.ard
new file mode 100644
index 00000000..d661f289
--- /dev/null
+++ b/src/Algebra/Group/Representation/Irreducible.ard
@@ -0,0 +1,21 @@
+\import Algebra.Group
+\import Algebra.Group.Representation.Category
+\import Algebra.Group.Representation
+\import Algebra.Group.Representation.Sub
+\import Algebra.Module.Category
+\import Algebra.Module.LinearMap
+\import Algebra.Ring
+\import Category
+\import Logic
+
+\func Irreducible {R : Ring}{G : Group} (E : LRepres R G) => \Pi(A : SubLRepres E) -> A.isTrivial
+
+\class Hom-between-Irreducible \noclassifying {R : Ring}{G : Group} {A B : LRepres R G}(p : Irreducible A)(q : Irreducible B){
+  \func Schur's-Lemma (f : InterwiningMap A B) : IsZeroMap f || Iso f => \case q (ImageSubLRepres f) \with {
+    | byLeft zero-image => byLeft (LinearMap.ZeroIm=>Zero-func zero-image)
+    | byRight full-image => \case p (KernelSubLRepres f) \with {
+      | byLeft zero-ker => byRight (repr+module-iso=>repr-iso (LinearMap.iso<->zeroKer-FullIm.2 (zero-ker, full-image)))
+      | byRight full-ker => byLeft (LinearMap.FullKer=>Zero-func full-ker)
+    }
+  }
+}
\ No newline at end of file
diff --git a/src/Algebra/Group/Representation/MaschkeLemma.ard b/src/Algebra/Group/Representation/MaschkeLemma.ard
new file mode 100644
index 00000000..17ef9150
--- /dev/null
+++ b/src/Algebra/Group/Representation/MaschkeLemma.ard
@@ -0,0 +1,158 @@
+\import Algebra.Group
+\import Algebra.Group.GSet
+\import Algebra.Group.Representation.Category
+\import Algebra.Group.Representation
+\import Algebra.Group.Representation.Sub
+\import Algebra.Module
+\import Algebra.Module.Category
+\import Algebra.Module.LinearMap
+\import Algebra.Monoid
+\import Algebra.Ring
+\import Category
+\import Category.PreAdditive
+\import Data.Array
+\import Equiv
+\import Function \hiding (id, o)
+\import Function.Meta
+\import Logic
+\import Meta \hiding (in)
+\import Paths
+\import Paths.Meta
+\import Set.Fin
+
+\class Maschke'sLemma{R : CRing}{G : FinGroup}{|G|^-1 : R}(q : R.natCoef G.finCard R.* |G|^-1 = R.ide)
+                     {E : LRepres R G}{S : SubLRepres E}{
+
+  \func mean_func {E W : LRepres R G} (f : LinearMap E W):
+    InterwiningMap E W => LModule.*c |G|^-1 (SumOverGroup f)
+
+  \func retracts (p : SplitMono {LModuleCat R} S.in) : SplitMono {RepresentationCat R G} {S} {E} S.in \cowith
+    | hinv => mean_func p.hinv
+    | hinv_f => exts \lam e => rewrite (mean-func-preserve p-hinv-decypher e) idp
+    \where {
+      \func p-hinv-decypher (s : S) : p.hinv (S.in s) = s => path (\lam i => (p.hinv_f i) s)
+        }
+
+  \func mean-func-preserve {f : LinearMap E S} (p : \Pi(s : S) -> f (S.in s) = s) (t : S)
+    : mean_func f (S.in t) = t =>
+    unfold (rewrite (SumOverGroup-multiply, inv $ LModule.*c-assoc {S.S}, R.*-comm, q, ide_*c) idp)
+    \where {
+
+    \func SumOverGroup-multiply : SumOverGroup f (S.in t) = R.natCoef G.finCard *c t
+            => rewrite (SumOverGroup_same-elements, SumOverGroup.FinSumEqual-multiply t) idp
+    \where {
+      \func SumOverGroup_Sub :  SumOverGroup f (S.in t) = AbMonoid.FinSum {S}
+        (\lam (g : G) => g S.**'in f (inverse {G} g E.** S.in t)) => SumOverGroup.FinSumRewrite (\lam g => SumOverGroup.adjust g f) (in {S} t)
+
+      \func SumOverGroup_same-elements :
+        SumOverGroup f (S.in t) = AbMonoid.FinSum {S} (\lam (_ : G) => t)
+        => rewrite (SumOverGroup_Sub, SumOverGroup.FinSumEquality (\lam (g : G) => SumOverGroup_subrepr-property g t)) idp
+
+      \func SumOverGroup_subrepr-property (g : G) (t : S) : g S.**'in f (inverse g E.** S.in t) = t
+        => rewrite (inv $ InterwiningMap.func-** {S.in}, p (inverse g S.**'in t), **-assoc, G.inverse-right, id-action) idp
+    }
+
+    }
+}
+
+
+
+{- | It is a function that given a linear map $f : A \to B$ between two representations of a finite group $G$
+produces an interwining linear map $f'$ via the following formula
+ $f' a := \sum_{g : G} g f (g^{ -1} a)$
+ -}
+\func SumOverGroup{R : CRing}{G : FinGroup} {A B : LRepres R G}(f : LinearMap A B) : InterwiningMap A B \cowith
+  | LinearMap => int
+  | func-** {a} {h} => rewrite (bring_h_out h a, inv $ ap-rearrange h a) idp
+  \where {
+    \func Ab : AbGroup => PreAdditivePrecat.AbHom {LModulePreAdditive R} {A} {B}
+
+    \func adjust(g : G) (f : LinearMap A B) : LinearMap A B \cowith
+      | func a => g B.** f ( inverse g A.** a)
+      | func-+ => rewrite (A.**-ldistr, f.func-+, B.**-ldistr) idp
+      | func-*c => rewrite (A.**-*c, f.func-*c, B.**-*c) idp
+
+    \func adjust' : G -> LinearMap A B => \lam g => adjust g f
+
+    \func int : LinearMap A B => Ab.FinSum (\lam (g : G) => adjust g f)
+
+    \func group_prop (g h : G)(a : A) : adjust g f (h A.** a) = h B.** adjust (inverse h * g) f a
+      => unfold (inv (rewrite (B.**-assoc, inv G.*-assoc, G.inverse-right, G.ide-left, G.inverse_*, G.inverse-isInv, A.**-assoc) idp))
+
+    \func FinSum-equivariance (h : G) {x : G -> B} : h B.** B.FinSum x = B.FinSum (\lam z => h B.** x z)
+      => \case B.FinSum_char x  \with {
+        | inP p => rewrite (p.2, B.FinSum_char2 (h B.** x __) p.1, BigSum-equivariance) idp
+      }
+      \where {
+        \func act_array (h : G)(e : Array B) : Array B => \lam i => h B.** e i
+
+        \func BigSum-equivariance (e : Array B) : h B.** B.BigSum e = B.BigSum (act_array h e) \elim e
+          | nil => rewrite B.g**-zro idp
+          | a :: l => rewrite (B.**-ldistr, BigSum-equivariance l) idp
+      }
+
+    \func FinSumEquality {E : AbMonoid} {A : FinSet} {x y : A -> E} (eq : \Pi (a : A) -> x a = y a)
+      : E.FinSum x = E.FinSum y => \case E.FinSum_char x \with {
+      | inP a => rewrite (a.2, E.FinSum_char2 y a.1, BigSumEquality) idp
+    }\where {
+      \func BigSumEquality {a : Equiv {Fin A.finCard} {A}}
+        : AddMonoid.BigSum (\new Array E A.finCard (\lam j => x (a j))) =
+      AddMonoid.BigSum (\new Array E A.finCard (\lam j => y (a j))) =>
+        pmap AddMonoid.BigSum ArrayEquality
+      \func ArrayEquality  {a : Equiv {Fin A.finCard} {A}}: (\new Array E A.finCard (\lam j => x (a j))) =
+      (\new Array E A.finCard (\lam j => y (a j))) => arrayExt (\lam j => eq (a j))
+    }
+
+    \func FinSumRewrite (x : G -> Ab) (a : A)
+      : (Ab.FinSum x) a = B.FinSum (\lam e => (x e) a) => \case Ab.FinSum_char x \with {
+      | inP a1 => rewrite (a1.2, B.FinSum_char2 (x __ a) a1.1, BigSumRewrite) idp
+    }
+      \where {
+        \func Ab_Helper {f g : Ab}{x : A} : (f + g) x = f x + g x => idp
+
+        \func ap_BigSum_el_wise (e : Array Ab)(a : A) : Array B => \lam i => (e i) a
+
+        \func BigSumRewrite (e : Array Ab)(a : A) : (Ab.BigSum e) a = B.BigSum (ap_BigSum_el_wise e a) \elim e
+          | nil => idp
+          | a1 :: l => rewrite (Ab_Helper, BigSumRewrite l a) idp
+      }
+
+    \lemma PermutationInvariance {E : AbMonoid}{A : FinSet}
+                                 (x : A -> E)(p : A -> A)(permute : QEquiv p): E.FinSum x  = E.FinSum {A} (x Function.o p)
+      => E.FinSum_Equiv {A}{A} permute
+
+    \lemma rearrange (h : G) : int = Ab.FinSum (\lam (g : G) => adjust (inverse h * g) f)
+      => PermutationInvariance adjust' (inverse h *) (Group.translate-is-Equiv (inverse h))
+
+    \lemma ap-rearrange (h : G) (a : A)
+      : int a = Ab.FinSum (\lam g => adjust (inverse h * g) f) a
+      => path \lam i => rearrange h i a
+
+    \func bring_h_out (h : G) (a : A)
+      : int (h A.** a) = h B.** (Ab.FinSum (\lam g => adjust (inverse h * g) f)) a
+      => inv $ rewrite (zero-2-step h a, FinSum-equivariance, step-4 h a, inv $ FinSumRewrite (adjust __ f) (h A.** a)) idp
+      \where {
+        \lemma zero-2-step (h : G)(a : A)
+          : Ab.FinSum (\lam g => adjust (G.inverse h G.* g) f) a = B.FinSum (\lam g => adjust (G.inverse h G.* g) f a)
+          => FinSumRewrite (\lam g => adjust (G.inverse h G.* g) f) a
+
+        \lemma step-4 (h : G) (a : A)
+          : B.FinSum (\lam g => h B.** adjust (inverse h * g) f a) =
+            B.FinSum (\lam g => g B.** f (inverse g A.** (h A.** a)))
+          => rewrite (FinSumEquality helper) idp
+          \where {
+            \func helper {h : G}{a : A}(g : G) : h B.** adjust (inverse h * g) f a = g B.** f (inverse g A.** (h A.** a))
+              => unfold $ rewrite (G.inverse_*, G.inverse-isInv, inv A.**-assoc, B.**-assoc, inv G.*-assoc, G.inverse-right, G.ide-left) idp
+          }
+
+      }
+    \func FinSumEqual-multiply {E : LModule R} {A : FinSet} (e : E) : E.FinSum (\lam (_ : A) => e) = R.natCoef A.finCard *c e =>
+      \case E.FinSum_char (\lam (_ : A) => e) \with {
+        | inP a => rewrite (a.2, BigSumEqual A.finCard) idp
+      }
+      \where {
+        \func BigSumEqual (n : Nat) : AddMonoid.BigSum (\new Array E n (\lam _ => e)) = R.natCoef n *c e \elim n
+          | 0 => rewrite (R.natCoefZero, E.*c_zro-left) idp
+          | suc n => rewrite (R.natCoefSuc n, E.*c-rdistr, inv $ BigSumEqual n, E.ide_*c, E.+-comm) idp
+      }
+  }
\ No newline at end of file
diff --git a/src/Algebra/Group/Representation/PermutationRepresentation.ard b/src/Algebra/Group/Representation/PermutationRepresentation.ard
new file mode 100644
index 00000000..cbf543f2
--- /dev/null
+++ b/src/Algebra/Group/Representation/PermutationRepresentation.ard
@@ -0,0 +1,110 @@
+\import Algebra.Group
+\import Algebra.Group.GSet
+\import Algebra.Group.Representation.Category
+\import Algebra.Group.Representation.Irreducible
+\import Algebra.Group.Representation
+\import Algebra.Group.Representation.Sub
+\import Algebra.Module
+\import Algebra.Module.LinearMap
+\import Algebra.Module.PowerLModule
+\import Algebra.Monoid
+\import Algebra.Pointed
+\import Algebra.Ring
+\import Category.Functor \hiding (trans)
+\import Function.Meta ($)
+\import Logic
+\import Meta (cases, unfold)
+\import Paths
+\import Paths.Meta
+\import Set
+
+{- | Action given as $$g \cdot \left( \sum \lambda_i x_i \right) := \sum \lambda_{g^{-1}(i)}x_i $$  for a basis of $x_i$'s -} -}
+\func PermRepr {R : Ring} {G : Group} (X : GroupAction G) : LRepres R G \cowith
+  | LModule => Module
+  | ** g f j => f (inverse g X.** j)
+  | **-assoc => ext (\lam _ => rewrite (X.**-assoc, inverse_prod) idp)
+  | **-ldistr => idp
+  | **-*c => ext (\lam _ => idp)
+  | id-action => ext (\lam _ => rewrite (G.inverse_ide, X.id-action) idp)
+  \where{
+    \func inverse_prod {m n : G} : inverse (m * n) = inverse n * inverse m =>
+      inv (G.check-for-inv ( rewrite (G.*-assoc, pmap (m `*) (inv G.*-assoc) , G.inverse-right, G.ide-left, G.inverse-right) idp))
+    \func R_m : LModule R => RingLModule R
+    \func Module : LModule R => PowerLModule X R_m -- product module of |X| copies of R
+  }
+
+{- |
+Here we prove that $span(1, 1, \ldots)$ is an invariant and non-trivial subspace in $\prod_X R$ as an $R$-module.
+For this proof to work one needs to know that there are at least two points in $X$.
+Also, without some decidability constraint for X this fact will not be true
+(one cannot prove that representation of $G = \mathbb{Z}$ over $R = \mathbb{Z}$ induced by action of
+$\mathbb{Z}$ on $\mathbb{R}$ by translations is reducible. That is because one cannot construct
+a non-constant function $\mathbb{R} \to \mathbb{Z}$ in constructive mathematics).
+Also, this does not make much sense over a trivial ring, thus we eliminate this case as well.
+ -}
+\class PermutationRepresReducible {R : Ring} {G : Group} (X : GroupAction G) {
+  | somepoint : X
+  | somepoint' : X
+  | different-points : somepoint' /= somepoint
+  | not-trivial-ring : R.zro /= R.ide
+  | decideEq-somepoint (x : X) : Dec (x = somepoint)
+  \func somepoints-equality-1 : decideEq-somepoint somepoint = yes idp => cases (decideEq-somepoint somepoint) \with {
+    | yes e => exts
+    | no n => absurd (n idp)
+  }
+  \func somepoints-equality-2 : decideEq-somepoint somepoint' = no different-points => cases (decideEq-somepoint somepoint') \with {
+    | yes e => absurd (different-points e)
+    | no n => exts
+  }
+  -- basic definitions to work easier
+  \func R_m : LModule R => RingLModule R
+  \func R_m-triv : LRepres R G => TrivialAction R_m G
+
+  \func Module : LModule R => PowerLModule X R_m -- product module of |X| copies of R
+  \func Repr : LRepres R G => PermRepr {R} {G} X
+  \func vectorOnes : Module => \lam _ => R.ide -- vector with coordinates (1,1,1,...)
+
+  \func invSubMod : LinearMap R_m Module \cowith
+    | func (r : R) => \lam _ => r
+    | func-+ => ext (\lam _ => idp)
+    | func-*c => ext (\lam _ => idp)
+
+  \func inv-rev (r : R_m-triv)  : (invSubMod r) somepoint = r => idp
+
+
+  \func fixed-submodule (g : G) (r : R) : g Repr.** invSubMod r = invSubMod r => ext (\lam j => aux r j (inverse g X.** j) )
+      \where{
+        \func aux(r : R)(j j' : X) : invSubMod r j = invSubMod r j' => idp
+      }
+
+  \func invSubRepr : SubLRepres Repr \cowith
+    | S => R_m-triv
+    | in => \new InterwiningMap {
+      | LinearMap => invSubMod
+      | func-** {e : R_m-triv}{g : G} => ext (\lam _ => rewrite (fixed-submodule g e) idp)
+    }
+    | in-mono => \lam {a a' : R} (p : invSubMod a = invSubMod a') => rewrite (inv (inv-rev a), inv (inv-rev a'), p) idp
+
+\func Non-constant-vector : Repr => \lam (j : X) => \case decideEq-somepoint j \with {
+  | yes e => R.ide
+  | no n => R.zro
+}\where {
+    \func equation-1 : Non-constant-vector somepoint = R.ide => unfold Non-constant-vector $ rewrite somepoints-equality-1 idp
+    \func equation-2 : Non-constant-vector somepoint' = R.zro => unfold Non-constant-vector $ rewrite somepoints-equality-2 idp
+  }
+
+{- | We prove that $span(1,1,\ldots)$ is neither zero submodule nor does it
+   - contain the whole space. To prove the second claim we show that
+  Non-constant-vector does not lie in the image of invSubMod map.  -}
+  \func SubRepr-non-trivial : Not invSubRepr.isTrivial => \lam p => \case \elim p \with {
+    | byLeft zeromod => not-trivial-ring (inv (zeromod R.ide))
+    | byRight isSurj-in => \case isSurj-in Non-constant-vector \with {
+      | inP a => not-trivial-ring (rewrite (inv Non-constant-vector.equation-1,
+                                            inv Non-constant-vector.equation-2, inv a.2, fixed-submodule.aux a.1 somepoint' somepoint) idp)
+    }
+  }
+
+  \func Not-Irreducible : Not (Irreducible Repr) => \lam prf-irred => SubRepr-non-trivial (prf-irred invSubRepr)
+
+}
+
diff --git a/src/Algebra/Group/Representation/Product.ard b/src/Algebra/Group/Representation/Product.ard
new file mode 100644
index 00000000..606ad809
--- /dev/null
+++ b/src/Algebra/Group/Representation/Product.ard
@@ -0,0 +1,56 @@
+\import Algebra.Group
+\import Algebra.Group.Representation.Category
+\import Algebra.Group.Representation
+\import Algebra.Meta
+\import Algebra.Module
+\import Algebra.Module.LinearMap
+\import Algebra.Ring
+\import Function.Meta
+\import Paths
+\import Paths.Meta
+
+\func ProductLRepres {R : Ring} {G : Group} (A B : LRepres R G) : LRepres R G \cowith
+  | LModule => ProductLModule R A B
+  | ** g (a, b) => (g A.** a, g B.** b)
+  | **-assoc => rewrite (A.**-assoc, B.**-assoc) idp
+  | id-action => rewrite (A.id-action, B.id-action) idp
+  | **-ldistr => rewrite (A.**-ldistr, B.**-ldistr) idp
+  | **-*c => rewrite (A.**-*c, B.**-*c) idp
+  \where {
+    \func in_1 {R : Ring} {G : Group} (A B : LRepres R G) : InterwiningMap A (ProductLRepres A B) \cowith
+      | func a => (a, 0)
+      | func-+ {a}{b} => rewrite (pmap (\lam z => (a A.+ b, z)) (inv B.zro-right)) idp
+      | func-*c{r} {_} => rewrite (inv $ B.*c_zro-right {r}, inv aux, B.*c_zro-right) idp
+      | func-** {e} {g} => rewrite (pmap (\lam z => (g A.** e, z) )(inv $ B.g**-zro {g})) idp
+      \where {
+        \func aux {r : R}{a : A}{b : B} : r *c (a, b) = (r *c a, r *c b) => idp
+      }
+    \func in_2 {R : Ring} {G : Group} (A B : LRepres R G) : InterwiningMap B (ProductLRepres A B) \cowith
+      | func b => (0, b)
+      | func-+ {a}{b} => rewrite (pmap (\lam z => (z, a B.+ b)) (inv A.zro-right)) idp
+      | func-*c {r} {_} => rewrite (inv $ A.*c_zro-right {r}, inv aux, A.*c_zro-right) idp
+      | func-** {e} {g} => rewrite (pmap (\lam z => (z, g B.** e) )(inv $ A.g**-zro {g})) idp
+      \where {
+        \func aux {r : R}{a : A}{b : B} : r *c (a, b) = (r *c a, r *c b) => idp
+      }
+
+    \func proj_1{R : Ring} {G : Group} (A B : LRepres R G) : InterwiningMap (ProductLRepres A B) A \cowith
+      | func (a, b) => a
+      | func-** => idp
+      | func-+ => idp
+      | func-*c => idp
+
+    \func proj_2{R : Ring} {G : Group} (A B : LRepres R G) : InterwiningMap (ProductLRepres A B) B \cowith
+      | func (a, b) => b
+      | func-** => idp
+      | func-+ => idp
+      | func-*c => idp
+
+    \func coprod-map{R : Ring} {G : Group} {A B C : LRepres R G}(i : InterwiningMap A C)(j : InterwiningMap B C) : InterwiningMap (ProductLRepres A B) C \cowith
+      | func (a, b) => i a C.+ j b
+      | func-+ => rewrite (i.func-+, j.func-+) equation
+      | func-*c => rewrite (i.func-*c, j.func-*c, C.*c-ldistr) idp
+      | func-** => rewrite (i.func-**, j.func-**, C.**-ldistr) idp
+  }
+
+
diff --git a/src/Algebra/Group/Representation/Sub.ard b/src/Algebra/Group/Representation/Sub.ard
new file mode 100644
index 00000000..eb226789
--- /dev/null
+++ b/src/Algebra/Group/Representation/Sub.ard
@@ -0,0 +1,28 @@
+\import Algebra.Group
+\import Algebra.Group.Representation.Category
+\import Algebra.Group.Representation
+\import Algebra.Module.Category
+\import Algebra.Ring
+\import Function
+\import Logic
+\import Paths.Meta
+
+\class SubLRepres {R : Ring} {G : Group} (E : LRepres R G) (\classifying S : LRepres R G ){
+  | in : InterwiningMap S E
+  | in-mono : isInj in
+
+  \func isTrivial => IsZeroMod S || isSurj in
+
+  \func \infix 7 **'in (g : G)(s : S) : S => (LinRepres.** {S}) g s
+
+}
+
+\func KernelSubLRepres{R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : SubLRepres A \cowith
+  | S => KerLRepres f
+  | in => KerLRepresHom f
+  | in-mono {a a' : KerLRepres f} => \lam (p : KerLRepresHom f a = KerLRepresHom f a') => exts p
+
+\func ImageSubLRepres {R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : SubLRepres B \cowith
+  | S => ImageLRepres {R} {G} {A} {B} f
+  | in => ImageLRepresRightHom f
+  | in-mono {a a' : ImageLRepres f} => \lam (p : ImageLRepresRightHom f a = ImageLRepresRightHom f a') => ext p
diff --git a/src/Algebra/Group/Sub.ard b/src/Algebra/Group/Sub.ard
index 7cb2b2cb..6993be6b 100644
--- a/src/Algebra/Group/Sub.ard
+++ b/src/Algebra/Group/Sub.ard
@@ -3,17 +3,14 @@
 \import Algebra.Monoid
 \import Algebra.Monoid.Sub
 \import Algebra.Pointed
-\import Data.Bool
-\import Equiv
 \import Function
 \import Function.Meta
 \import Logic
-\import Logic.Meta
 \import Meta
+\import Order.PartialOrder
 \import Paths
 \import Paths.Meta
 \import Relation.Equivalence
-\import Order.PartialOrder
 \import Set
 \import Set.Category
 \open Group
@@ -107,7 +104,7 @@
 \class NormalSubGroup \extends SubGroup {
   | isNormal (g : S) {h : S} : contains h -> contains (conjugate g h)
 
-  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains ((inverse g) * h * g)
+  \lemma isNormal' (g : S) {h : S} (c : contains h) : contains (inverse g * h * g)
     => simplify in isNormal (inverse g) c
 
   \func quotient : Group Cosets \cowith
diff --git a/src/Algebra/Module.ard b/src/Algebra/Module.ard
index e455bd63..ff8e9672 100644
--- a/src/Algebra/Module.ard
+++ b/src/Algebra/Module.ard
@@ -11,6 +11,7 @@
 \import Algebra.Semiring
 \import Arith.Nat
 \import Category
+\import Category.Functor
 \import Data.Array
 \import Data.Fin (unfsuc)
 \import Equiv
@@ -27,6 +28,7 @@
 \import Paths
 \import Paths.Meta
 \import Set
+\import Set.Category
 \import Set.Fin
 
 \class LModule (R : Ring) \extends AbGroup {
@@ -354,6 +356,44 @@
   | *c-ldistr => pmap2 (__,__) *c-ldistr *c-ldistr
   | *c-rdistr => pmap2 (__,__) *c-rdistr *c-rdistr
   | ide_*c => pmap2 (__,__) ide_*c ide_*c
+  \where {
+    \func in1 {R : Ring} (A B : LModule R) : LinearMap A (ProductLModule R A B) \cowith
+      | func a => (a, 0)
+      | func-+ {a} {b} => rewrite (pmap (\lam z => (a A.+ b, z)) (inv B.zro-right)) idp
+      | func-*c{r} {_} => rewrite (inv $ B.*c_zro-right {r}, inv aux, B.*c_zro-right) idp
+      \where {
+        \private \lemma aux {r : R} {a : A} {b : B} : r LModule.*c {ProductLModule R A B} (a, b) = (r *c a, r *c b) => idp
+      }
+
+    \func in2 {R : Ring} (A B : LModule R) : LinearMap B (ProductLModule R A B) \cowith
+      | func b => (0, b)
+      | func-+ {a} {b} => rewrite (pmap (\lam z => (z, a B.+ b)) (inv A.zro-right)) idp
+      | func-*c {r} {_} => rewrite (inv $ A.*c_zro-right {r}, inv aux, A.*c_zro-right) idp
+      \where {
+        \private \lemma aux {r : R} {a : A} {b : B} : r LModule.*c {ProductLModule R A B} (a, b) = (r *c a, r *c b) => idp
+      }
+
+    \func proj1 {R : Ring} (A B : LModule R) : LinearMap (ProductLModule R A B) A \cowith
+      | func (a, b) => a
+      | func-+ => idp
+      | func-*c => idp
+
+    \func proj2 {R : Ring} (A B : LModule R) : LinearMap (ProductLModule R A B) B \cowith
+      | func (a, b) => b
+      | func-+ => idp
+      | func-*c => idp
+
+    \func coprod-map {R : Ring} {A B C : LModule R} (i : LinearMap A C) (j : LinearMap B C) : LinearMap (ProductLModule R A B) C \cowith
+      | func (a, b) => i a C.+ j b
+      | func-+ => rewrite (i.func-+, j.func-+) equation
+      | func-*c => rewrite (i.func-*c, j.func-*c, C.*c-ldistr) idp
+
+    \func prod-map {R : Ring} {A B C : LModule R} (a : LinearMap C A) (b : LinearMap C B) : LinearMap C (ProductLModule R A B) \cowith
+      | func c => (a c, b c)
+      | func-+ => rewrite (a.func-+, b.func-+) idp
+      | func-*c => rewrite (a.func-*c, b.func-*c) idp
+  }
+
 
 \func RingLModule (R : Ring) : LModule R R \cowith
   | AbGroup => R
@@ -377,20 +417,6 @@
       => (\lam c p (0) => inv ide-right *> inv zro-right *> p, \lam x => inP (x :: nil, simplify))
   }
 
-\instance PowerLModule {R : Ring} (J : \Set) (M : LModule R) : LModule R (J -> M)
-  | zro _ => 0
-  | + f g j => f j + g j
-  | zro-left => ext (\lam j => zro-left)
-  | zro-right => ext (\lam j => zro-right)
-  | +-assoc => ext (\lam j => +-assoc)
-  | negative f j => negative (f j)
-  | negative-left => ext (\lam j => negative-left)
-  | +-comm => ext (\lam j => +-comm)
-  | *c r f j => r *c f j
-  | *c-assoc => ext (\lam j => *c-assoc)
-  | *c-ldistr => ext (\lam j => *c-ldistr)
-  | *c-rdistr => ext (\lam j => *c-rdistr)
-  | ide_*c => ext (\lam j => ide_*c)
 
 \instance ArrayLModule {R : Ring} (n : Nat) (M : LModule R) : LModule R (Array M n)
   | zro _ => 0
diff --git a/src/Algebra/Module/Category.ard b/src/Algebra/Module/Category.ard
index f3520177..bcc8ea7d 100644
--- a/src/Algebra/Module/Category.ard
+++ b/src/Algebra/Module/Category.ard
@@ -1,11 +1,16 @@
+\import Algebra.Group
 \import Algebra.Group.Category
+\import Algebra.Meta
 \import Algebra.Module
 \import Algebra.Module.LinearMap
+\import Algebra.Module.Sub
 \import Algebra.Monoid.Category
 \import Algebra.Ring
 \import Algebra.Ring.RingHom
 \import Category
 \import Category.Meta
+\import Category.PreAdditive
+\import Function (isInj)
 \import Logic
 \import Paths
 \import Paths.Meta
@@ -26,6 +31,61 @@
   | id-right => idp
   | o-assoc => idp
   | univalence => sip (\lam (f : LinearMap) g => exts (f.func-zro, \lam x x' => f.func-+, \lam x => f.func-negative, \lam e x => f.func-*c))
+\where {
+  \func in {N : LModule R} (S : SubLModule R N) : LinearMap S.struct N \cowith
+    | func x => x.1
+    | func-+ => idp
+    | func-*c => idp
+
+  \lemma in-mono {N : LModule R} (S : SubLModule R N) : isInj (in S) => \lam p => exts p
+}
+
+\instance LModulePreAdditive (R : Ring) : PreAdditivePrecat \cowith
+  | Precat => LModuleCat R
+  | AbHom => \new AbGroup {
+    | zro => zeroMap
+    | + => addMaps
+    | zro-left => exts \lam _ => LModule.zro-left
+    | zro-right => exts \lam _ => LModule.zro-right
+    | +-assoc => exts \lam _ => LModule.+-assoc
+    | negative => negativeMap
+    | negative-left => exts \lam _ => LModule.negative-left
+    | +-comm => exts \lam _ => LModule.+-comm
+  }
+  | l-bilinear => exts \lam _ => LinearMap.func-+
+  | r-bilinear => exts \lam _ => idp
+  \where {
+    \func zeroMap {M N : LModule R} : LinearMap M N \cowith
+      | func _ => N.zro
+      | func-+ => inv N.zro-right
+      | func-*c => inv N.*c_zro-right
+
+    \func addMaps {M N : LModule R} (f g : LinearMap M N)  : LinearMap M N \cowith
+      | func m => f m N.+ g m
+      | func-+ => rewrite (f.func-+, g.func-+) equation
+      | func-*c => rewrite (f.func-*c, g.func-*c, N.*c-ldistr) idp
+
+    \func negativeMap {M N : LModule R} (f : LinearMap M N) : LinearMap M N \cowith
+      | func m => negative (f m)
+      | func-+ => rewrite (f.func-+, inv N.neg_ide_*c, inv N.neg_ide_*c, inv N.neg_ide_*c, N.*c-ldistr) idp
+      | func-*c => rewrite (f.func-*c, inv N.neg_ide_*c, inv N.neg_ide_*c, inv N.*c-assoc, inv N.*c-assoc, R.negative_ide-right, R.negative_ide-left) idp
+  }
+
+\instance LinearMapLModule {R : CRing} (A B : LModule R) : LModule R \cowith
+  | AbGroup => AbHom {LModulePreAdditive R} {A} {B}
+  | *c (c : R) (f : LinearMap A B) : LinearMap A B \cowith {
+    | func a => c B.*c f a
+    | func-+ => rewrite (f.func-+, B.*c-ldistr) idp
+    | func-*c => rewrite (f.func-*c, inv B.*c-assoc, inv B.*c-assoc, R.*-comm) idp
+  }
+  | *c-assoc => exts \lam _ => B.*c-assoc
+  | *c-ldistr => exts \lam _ => B.*c-ldistr
+  | *c-rdistr => exts \lam _ => B.*c-rdistr
+  | ide_*c => exts \lam _ => B.ide_*c
+
+\func IsZeroMod {R : Ring} (M : LModule R) => \Pi (m : M) -> m = 0
+
+\func IsZeroMap {R : Ring} {M N : LModule R} (f : LinearMap M N) => \Pi (m : M) -> f m = 0
 
 \instance KerLModule {R : Ring} {A B : LModule R} (f : LinearMap A B) : LModule R
   | AbGroup => KerAbGroup f
@@ -35,7 +95,7 @@
   | *c-rdistr => ext *c-rdistr
   | ide_*c => ext ide_*c
 
-\func KerLModuleHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (KerLModule f) f.Dom \cowith
+\func KerLModuleHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (KerLModule f) A \cowith
   | AddGroupHom => KerGroupHom f
   | func-*c => idp
 
@@ -47,29 +107,29 @@
   | *c-rdistr => ext *c-rdistr
   | ide_*c => ext ide_*c
 
-\func ImageLModuleLeftHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap f.Dom (ImageLModule f) \cowith
-  | AddGroupHom => ImageGroupLeftHom f
+\func ImageLModuleLeftHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap A (ImageLModule f) \cowith
+  | AddGroupHom => ImageAddGroupLeftHom f
   | func-*c => ext func-*c
 
-\func ImageLModuleRightHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (ImageLModule f) f.Cod \cowith
-  | AddGroupHom => ImageGroupRightHom f
+\func ImageLModuleRightHom {R : Ring} {A B : LModule R} (f : LinearMap A B) : LinearMap (ImageLModule f) B \cowith
+  | AddGroupHom => ImageAddGroupRightHom f
   | func-*c => idp
 
 \instance LinearMapRing {R : Ring} (U : LModule R) : Ring (LinearMap U U)
   | zro => linearMap_zro
   | + => linearMap_+
-  | zro-left => exts \lam u => U.zro-left
-  | +-assoc => exts \lam u => U.+-assoc
-  | +-comm => exts \lam u => U.+-comm
+  | zro-left => exts \lam _ => U.zro-left
+  | +-assoc => exts \lam _ => U.+-assoc
+  | +-comm => exts \lam _ => U.+-comm
   | negative => linearMap_negative
-  | negative-left => exts \lam u => U.negative-left
-  | ide => id U
+  | negative-left => exts \lam _ => U.negative-left
+  | ide => id {LModuleCat R} U
   | * f g => g ∘ f
   | ide-left => idp
   | ide-right => idp
   | *-assoc => idp
   | ldistr => idp
-  | rdistr => exts \lam u => func-+
+  | rdistr => exts \lam _ => func-+
   \where {
     \func *c-hom {R : CRing} {U : LModule R} : RingHom R (LinearMapRing U) \cowith
       | func (r : R) : LinearMap U U \cowith {
@@ -77,7 +137,7 @@
         | func-+ => *c-ldistr
         | func-*c => inv *c-assoc *> pmap (`*c _) R.*-comm *> *c-assoc
       }
-      | func-+ => exts \lam u => *c-rdistr
-      | func-ide => exts \lam u => ide_*c
+      | func-+ => exts \lam _ => *c-rdistr
+      | func-ide => exts \lam _ => ide_*c
       | func-* => exts \lam u => pmap (`*c u) R.*-comm *> *c-assoc
   }
diff --git a/src/Algebra/Module/LinearMap.ard b/src/Algebra/Module/LinearMap.ard
index 737756ea..05b6ab49 100644
--- a/src/Algebra/Module/LinearMap.ard
+++ b/src/Algebra/Module/LinearMap.ard
@@ -159,6 +159,41 @@
                     | f_hinv => exts e.f_ret
                   })
 
+  \func ZeroIm=>Zero-func {R : Ring} {M N : LModule R} {f : LinearMap M N} (p : IsZeroMod (ImageLModule f)) : IsZeroMap f
+    => \lam (m : M) => rewrite (inv (aux-2 m), p (aux-1 m), LinearMap.func-zro {ImageLModuleRightHom f}) idp
+    \where{
+      \func aux-1 (m : M) : ImageLModule f => (f m , inP(m ,idp))
+      \func aux-2 (m : M) : ImageLModuleRightHom f (aux-1 m) = f m => idp
+    }
+
+  \func FullKer=>Zero-func{R : Ring} {M N : LModule R} {f : LinearMap M N} (p : isSurj (KerLModuleHom f)) : IsZeroMap f
+    => \lam (m : M) => \case  p m \with {
+      | inP a => rewrite (inv a.2, a.1.2) idp
+    }
+
+  \func zeroKer-FullIm<->inj+surj{R : Ring} {M N : LModule R} {f : LinearMap M N}:
+    (\Sigma (isInj f) (isSurj f)) <-> (\Sigma (IsZeroMod (KerLModule f)) (isSurj (ImageLModuleRightHom f)))
+    => (\lam p => (inj->zeroKer p.1, surj->FullIm p.2),
+        \lam p => (zeroKer->inj p.1, FullIm->surj p.2)
+    )
+    \where{
+      \func inj->zeroKer (p : isInj f) : IsZeroMod (KerLModule f) => \lam (a : KerLModule f) =>
+          ext (p {a.1} {M.zro} (rewrite (a.2, f.func-zro) idp))
+      \func surj->FullIm (p : isSurj f) : isSurj (ImageLModuleRightHom f) => \lam (n : N) =>
+          TruncP.map (p n) \lam s => ((n, inP s), idp)
+      \func zeroKer->inj (w : IsZeroMod (KerLModule f)) : isInj f => \lam {a b : M} (p : f a = f b) =>
+          M.fromZero (simple-lemma3 (a - b, rewrite (f.func-minus, N.toZero p ) idp) (w (a - b, rewrite (f.func-minus, N.toZero p ) idp))) -- ext (w (a - b, rewrite (f.func-minus, simple-lemma2 p ) idp))
+      \func FullIm->surj (p : isSurj (ImageLModuleRightHom f)) : isSurj f => \lam (n : N) =>
+          \case p n \with {
+            | inP a => TruncP.map a.1.2 \lam s => (s.1, rewrite (s.2, a.2) idp)
+          }
+      \func simple-lemma3 (x : KerLModule f)(p : x = LModule.zro {KerLModule f}) : x.1 = LModule.zro {M} => pmap (\lam q => q.1) p
+    }
+
+  \lemma iso<->zeroKer-FullIm{R : Ring} {M N : LModule R} {f : LinearMap M N} :
+    Iso f <-> (\Sigma (IsZeroMod (KerLModule f)) (isSurj (ImageLModuleRightHom f))) => <->trans LinearMap.iso<->inj+surj zeroKer-FullIm<->inj+surj
+
+
   \lemma iso-basis {R : Ring} {U V : LModule R} (f : Iso {_} {U} {V}) {l : Array U} (lb : U.IsBasis l) : V.IsBasis (map f.f l)
     => (\lam c p j => lb.1 c ((iso<->inj+surj.1 f).1 $ func-BigSum *> pmap BigSum (exts \lam j => func-*c) *> p *> inv func-zro) j,
         \lam v => TruncP.map (lb.2 (f.hinv v)) \lam s => (s.1, (iso<->inj+surj.1 f.reverse).1 $ s.2 *> pmap BigSum (exts \lam j => inv $ func-*c *> path (\lam i => _ *c f.hinv_f i (l j))) *> inv func-BigSum))
diff --git a/src/Algebra/Module/PowerLModule.ard b/src/Algebra/Module/PowerLModule.ard
new file mode 100644
index 00000000..b3ea1f9f
--- /dev/null
+++ b/src/Algebra/Module/PowerLModule.ard
@@ -0,0 +1,32 @@
+\import Algebra.Module
+\import Algebra.Module.Category
+\import Algebra.Module.LinearMap
+\import Algebra.Ring
+\import Category.Functor
+\import Paths.Meta
+\import Set.Category
+
+\instance PowerLModule {R : Ring} (J : \Set) (M : LModule R) : LModule R (J -> M)
+  | zro _ => 0
+  | + f g j => f j M.+ g j
+  | zro-left => ext (\lam j => M.zro-left)
+  | zro-right => ext (\lam j => M.zro-right)
+  | +-assoc => ext (\lam j => M.+-assoc)
+  | negative f j => M.negative (f j)
+  | negative-left => ext (\lam j => M.negative-left)
+  | +-comm => ext (\lam j => M.+-comm)
+  | *c r f j => r *c f j
+  | *c-assoc => ext (\lam j => *c-assoc)
+  | *c-ldistr => ext (\lam j => *c-ldistr)
+  | *c-rdistr => ext (\lam j => *c-rdistr)
+  | ide_*c => ext (\lam j => ide_*c)
+
+\func FunctorPowerLMod {R : Ring} : Functor SetCat.op (LModuleCat R) \cowith
+  | F I => PowerLModule I (RingLModule R)
+  | Func f => \new LinearMap {
+    | func r j => r (f j)
+    | func-+ => idp
+    | func-*c => idp
+  }
+  | Func-id => idp
+  | Func-o => idp
\ No newline at end of file
diff --git a/src/Algebra/Module/Sub.ard b/src/Algebra/Module/Sub.ard
index ec982071..6416f5d3 100644
--- a/src/Algebra/Module/Sub.ard
+++ b/src/Algebra/Module/Sub.ard
@@ -17,6 +17,15 @@
 \class SubLModule (R : Ring) \extends SubAddGroup {
   \override S : LModule R
   | contains_*c {a : R} {b : S} : contains b -> contains (a *c b)
+
+  \func struct : LModule R \cowith
+    | AddGroup => SubAddGroup.struct
+    | +-comm => ext +-comm
+    | *c r p => (r *c p.1, contains_*c p.2)
+    | *c-assoc => ext *c-assoc
+    | *c-ldistr => ext *c-ldistr
+    | *c-rdistr => ext *c-rdistr
+    | ide_*c => ext ide_*c
 }
 
 \func topSubLModule {R : Ring} (M : LModule R) : SubLModule { | R => R | S => M } \cowith
@@ -30,7 +39,7 @@
   | <= U V => \Pi {a : M} -> U a -> V a
   | <=-refl c => c
   | <=-transitive f g c => g (f c)
-  | <=-antisymmetric f g => exts \lam a => ext (f,g)
+  | <=-antisymmetric f g => exts \lam _ => ext (f,g)
   | meet (U V : SubLModule { | R => R | S => M }) : SubLModule { | R => R | S => M } \cowith {
     | contains a => \Sigma (U a) (V a)
     | contains_zro => (contains_zro, contains_zro)
@@ -48,5 +57,18 @@
   | contains a => ∃ (l : Array (\Sigma (x : R) (I x) M)) (a = M.BigSum (map (\lam s => s.1 *c s.3) l))
   | contains_zro => inP (nil,idp)
   | contains_+ (inP s) (inP t) => inP (s.1 ++ t.1, pmap2 (+) s.2 t.2 *> inv M.BigSum_++ *> pmap M.BigSum (inv (map_++ (\lam s => s.1 *c s.3))))
-  | contains_negative (inP s) => inP (map (later \lam t => (negative t.1, contains_negative t.2, t.3)) s.1, pmap negative s.2 *> M.BigSum_negative *> pmap M.BigSum (exts \lam j => inv M.*c_negative-left))
-  | contains_*c {a} {b} (inP s) => inP (map (later \lam t => (a * t.1, ideal-left t.2, t.3)) s.1, pmap (a *c) s.2 *> M.*c_BigSum-ldistr *> pmap M.BigSum (exts \lam j => inv M.*c-assoc))
\ No newline at end of file
+  | contains_negative (inP s) => inP (map (later \lam t => (negative t.1, contains_negative t.2, t.3)) s.1, pmap negative s.2 *> M.BigSum_negative *> pmap M.BigSum (exts \lam _ => inv M.*c_negative-left))
+  | contains_*c {a} {_} (inP s) => inP (map (later \lam t => (a * t.1, ideal-left t.2, t.3)) s.1, pmap (a *c) s.2 *> M.*c_BigSum-ldistr *> pmap M.BigSum (exts \lam _ => inv M.*c-assoc))
+
+\func OneDimSubmod {R : Ring} {L : LModule R} (v : L) : SubLModule R L \cowith
+  | contains u => ∃ (r : R) (r *c v = u)
+  | contains_zro => inP (0, L.*c_zro-left)
+  | contains_+ p q => \case \elim p, \elim q \with {
+    | inP r1, inP r2 => inP (r1.1 + r2.1, rewrite (*c-rdistr, r1.2, r2.2) idp)
+  }
+  | contains_negative p => \case \elim p \with {
+    | inP r => inP (negative r.1, rewrite (L.*c_negative-left, pmap negative r.2) idp)
+  }
+  | contains_*c {a} p => \case \elim p \with {
+    | inP r => inP (a * r.1, rewrite (*c-assoc, r.2) idp)
+  }
\ No newline at end of file
diff --git a/src/Algebra/Module/Trace.ard b/src/Algebra/Module/Trace.ard
new file mode 100644
index 00000000..92ab77be
--- /dev/null
+++ b/src/Algebra/Module/Trace.ard
@@ -0,0 +1,63 @@
+\import Algebra.Linear.Matrix
+\import Algebra.Module
+\import Algebra.Module.LinearMap
+\import Algebra.Monoid
+\import Algebra.Ring
+\import Data.Array
+\import Function.Meta
+\import Logic
+\import Meta
+\import Paths
+\import Paths.Meta
+\import Set
+
+\func Trace {R : Ring} {n : Nat} : LinearMap (MatrixModule R n n) (RingLModule R) \cowith
+  | func M => BigSumHom (diag M)
+  | func-+ => rewrite (diag.func-+, inv BigSumHom.func-+) idp
+  | func-*c => rewrite (diag.func-*c, inv BigSumHom.func-*c) idp
+  \where {
+    \func diag : LinearMap (MatrixModule R n n) (ArrayLModule n (RingLModule R)) \cowith
+      | func M => \lam i => M i i
+      | func-+ => exts \lam _ => idp
+      | func-*c => exts \lam _ => idp
+
+    \func BigSumHom : LinearMap (ArrayLModule n (RingLModule R)) (RingLModule R) \cowith
+      | func e => R.BigSum e
+      | func-+ => R.BigSum_+
+      | func-*c => inv LModule.*c_BigSum-ldistr
+  }
+
+\lemma Trace-transpose {R : Ring}{n : Nat} (M : MatrixModule R n n) : Trace M = Trace (transpose M)
+  => idp
+
+\open MatrixRing
+
+\func Trace-prod {R : CRing}{n m : Nat}(A : MatrixModule R n m)(B : MatrixModule R m n)
+  : Trace (A product B) = Trace (B product A)
+  => rewrite (Trace-prod-unfold A B, R.BigSum-transpose, Trace-prod-unfold B A, help) idp
+\where \protected {
+  \lemma help
+    : R.BigSum (\lam j => R.BigSum (\lam k => A k j R.* B j k)) =
+      R.BigSum (\lam i => R.BigSum (\lam j => B i j R.* A j i))
+    => R.BigSum-ext \lam j => R.BigSum-ext \lam i => R.*-comm
+
+  \lemma Trace-prod-unfold {R : Ring} {n m : Nat} (X : MatrixModule R n m) (Y : MatrixModule R m n)
+    : Trace (X product Y) = R.BigSum (\lam i => R.BigSum (\lam j => X i j R.* Y j i))
+    => idp
+}
+
+\lemma Trace-conjugation {R : CRing} {n : Nat} {A B : Matrix R n n} {T : Monoid.Inv B} : Trace (T.inv product A product B) = Trace A
+  => rewrite (Trace-prod (T.inv product A) B, inv $ product-assoc B T.inv A, T.inv-right, Ring.ide-left {MatrixRing R n}) idp
+
+\lemma Trace-diagonal {R : Ring} {l : Array R} : Trace (diagonal l) = R.BigSum l
+  => unfold (rewrite diag-diagonal idp)
+\where {
+  \lemma diag-diagonal {n : Nat} (l : Array R n) : Trace.diag (diagonal l) = l
+    => exts \lam _ => mcases \with {
+      | yes p => idp
+      | no n1 => absurd (n1 idp)
+    }
+}
+
+\lemma Trace-ide {R : Ring}{n : Nat} : Trace (Ring.ide {MatrixRing R n}) = R.natCoef n
+  => rewrite (Trace-diagonal {R} {replicate n R.ide}, R.BigSum_replicate1) idp
\ No newline at end of file
diff --git a/src/Algebra/Monoid.ard b/src/Algebra/Monoid.ard
index fc04f2ee..780a1c98 100644
--- a/src/Algebra/Monoid.ard
+++ b/src/Algebra/Monoid.ard
@@ -76,6 +76,7 @@
     | ide-right => ide-left
     | *-assoc => inv *-assoc
 } \where {
+
   \func equals {M N : Monoid} (p : M = {\Set} N) (q : \let f x => coe (p @) x right \in \Pi (x y : M) -> f (x * y) = f x * f y) : M = N
     => exts (p, ide-equality , q)
     \where {
@@ -332,6 +333,9 @@
 
   \func BigSum (l : Array E) => Big (+) zro l
 
+  \lemma BigSum-ext {n : Nat} {l l' : Array E n} (p : \Pi (i : Fin n) -> l i = l' i) : BigSum l = BigSum l'
+    => pmap BigSum (arrayExt p)
+
   \lemma BigSum_++ {l l' : Array E} : BigSum (l ++ l') = BigSum l + BigSum l' \elim l
     | nil => inv zro-left
     | :: a l => unfold BigSum (rewrite BigSum_++ (inv +-assoc))
diff --git a/src/Algebra/Monoid/Category.ard b/src/Algebra/Monoid/Category.ard
index 8dbf9d81..bb26a775 100644
--- a/src/Algebra/Monoid/Category.ard
+++ b/src/Algebra/Monoid/Category.ard
@@ -252,7 +252,7 @@
   | +-assoc => ext +-assoc
 
 \instance ImageMonoid (f : MonoidHom) : Monoid
-  | Pointed => ImageMulPointed f
+  | Pointed => ImagePointed f
   | * a b => (a.1 * b.1, \case a.2, b.2 \with {
     | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2)
   })
@@ -260,12 +260,21 @@
   | ide-right => ext ide-right
   | *-assoc => ext *-assoc
 
-\func ImageMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith
-  | AddPointedHom => ImagePointedLeftHom f
+\func ImageMonoidLeftHom(f : MonoidHom) : MonoidHom f.Dom (ImageMonoid f) \cowith
+  | PointedHom => ImagePointedLeftHom f
+  | func-* => ext func-*
+
+\func ImageMonoidRightHom (f : MonoidHom) : MonoidHom (ImageMonoid f) f.Cod \cowith
+  | PointedHom => ImagePointedRightHom f
+  | func-* => idp
+
+
+\func ImageAddMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith
+  | AddPointedHom => ImageAddPointedLeftHom f
   | func-+ => ext func-+
 
-\func ImageMonoidRightHom (f : AddMonoidHom) : AddMonoidHom (ImageAddMonoid f) f.Cod \cowith
-  | AddPointedHom => ImagePointedRightHom f
+\func ImageAddMonoidRightHom (f : AddMonoidHom) : AddMonoidHom (ImageAddMonoid f) f.Cod \cowith
+  | AddPointedHom => ImageAddPointedRightHom f
   | func-+ => idp
 
 \instance ImageAbMonoid {A : AddMonoid} {B : AbMonoid} (f : AddMonoidHom A B) : AbMonoid
diff --git a/src/Algebra/Monoid/FreeMonoid.ard b/src/Algebra/Monoid/FreeMonoid.ard
new file mode 100644
index 00000000..7bfd7bd6
--- /dev/null
+++ b/src/Algebra/Monoid/FreeMonoid.ard
@@ -0,0 +1,25 @@
+\import Algebra.Monoid
+\import Algebra.Monoid.Category
+\import Data.List
+\import Function
+\import Paths.Meta
+
+\func universalFreeMonoidMap {S : \Set} {M : Monoid} (in : S -> M) : MonoidHom (ListMonoid {S}) M \cowith
+  | func => extension
+  | func-ide => idp
+  | func-* => helper
+  \where {
+    \func extension (list : ListMonoid {S}) : M \elim  list
+      | nil => M.ide
+      | a :: l => in a * extension l
+
+    \func helper  {x y : List S}
+      : extension (x ++ y) = extension x M.* extension  y \elim x {
+      | nil => rewrite M.ide-left idp
+      | _ :: l => rewrite (M.*-assoc, helper {_} {_} {_} {l}) idp
+  }
+}
+
+\func isMonoidGenerated {M : Monoid} {S : \Set} (j : S -> M)
+  => isSurj (universalFreeMonoidMap j)
+
diff --git a/src/Algebra/Pointed/Category.ard b/src/Algebra/Pointed/Category.ard
index 6bc7f28a..bb12cca4 100644
--- a/src/Algebra/Pointed/Category.ard
+++ b/src/Algebra/Pointed/Category.ard
@@ -66,20 +66,30 @@
 \instance ImageAddPointed (f : AddPointedHom) : AddPointed (Image f)
   | zro => (0, inP (0, func-zro))
 
-\instance ImageMulPointed (f : PointedHom) : Pointed (Image f)
+\instance ImagePointed (f : PointedHom) : Pointed (Image f)
   | ide => (ide, inP (ide, func-ide))
 
 
-\func ImagePointedLeftHom (f : AddPointedHom) : AddPointedHom f.Dom (ImageAddPointed f) \cowith
+\func ImagePointedLeftHom (f : PointedHom)  : PointedHom f.Dom (ImagePointed f) \cowith
+  | func a => (f a, inP (a, idp))
+  | func-ide => ext func-ide
+
+\func ImagePointedRightHom(f : PointedHom) : PointedHom (ImagePointed f) f.Cod \cowith
+  | func => __.1
+  | func-ide => idp
+
+
+
+\func ImageAddPointedLeftHom (f : AddPointedHom) : AddPointedHom f.Dom (ImageAddPointed f) \cowith
   | func a => (f a, inP (a, idp))
   | func-zro => ext func-zro
 
-\func ImagePointedRightHom (f : AddPointedHom) : AddPointedHom (ImageAddPointed f) f.Cod \cowith
+\func ImageAddPointedRightHom (f : AddPointedHom) : AddPointedHom (ImageAddPointed f) f.Cod \cowith
   | func => __.1
   | func-zro => idp
 
-\lemma image-surj {f : AddPointedHom} : isSurj (ImagePointedLeftHom f)
+\lemma image-surj {f : AddPointedHom} : isSurj (ImageAddPointedLeftHom f)
   => \lam y => TruncP.map y.2 \lam s => (s.1, ext s.2)
 
-\lemma image-inj {f : AddPointedHom} : isInj (ImagePointedRightHom f)
+\lemma image-inj {f : AddPointedHom} : isInj (ImageAddPointedRightHom f)
   => \lam p => ext p
\ No newline at end of file
diff --git a/src/Algebra/Ring.ard b/src/Algebra/Ring.ard
index f38066c7..cdfee39a 100644
--- a/src/Algebra/Ring.ard
+++ b/src/Algebra/Ring.ard
@@ -23,6 +23,7 @@
 \import Set
 \import Set.Fin
 
+{- | Associative ring -}
 \class Ring \extends Semiring, AbGroup {
   | zro_*-left {x} => AddGroup.cancel-left (zro * x) (
     zro * x + zro * x ==< inv rdistr >==
diff --git a/src/Category/PreAdditive.ard b/src/Category/PreAdditive.ard
new file mode 100644
index 00000000..55a7e2f4
--- /dev/null
+++ b/src/Category/PreAdditive.ard
@@ -0,0 +1,52 @@
+\import Algebra.Group
+\import Algebra.Ring
+\import Algebra.Semiring
+\import Category
+\import Category.Limit
+\import Equiv (QEquiv)
+\import Equiv.Univalence (QEquiv-to-=)
+\import Function.Meta
+\import Paths
+\import Paths.Meta
+
+\class PreAdditivePrecat \extends Precat{
+  | AbHom {X Y : Ob} : AbGroup(Hom X Y)
+  | l-bilinear {X Y Z : Ob}{g h : Hom X Y}{f : Hom Y Z} : (g AbHom.+ h) >> f = g >> f AbHom.+  h >> f
+  | r-bilinear {X Y Z : Ob}{g h : Hom Y Z}{f : Hom X Y} : f >> (g AbHom.+ h) = f >> g AbHom.+  f >> h
+}
+
+\func Ring=OneObjectPreAdd : PreAdditivePrecat (\Sigma) = Ring => QEquiv-to-= \new QEquiv {
+  | f => PreAdditiveCategory-OneObject
+  | ret => Ring_toCat
+  | ret_f _ => idp
+  | f_sec _ => exts (idp, idp, \lam _ _  => idp, idp, \lam _ _ => idp, \lam _ => natCoefCoincide, \lam _ => idp)
+}
+  \where {
+    \func natCoefCoincide {b : Ring}{n : Nat} : natCoef {PreAdditiveCategory-OneObject (Ring_toCat b)} n = b.natCoef n \elim n
+      | 0 => rewrite b.natCoefZero idp
+      | suc n => rewrite (b.natCoefSuc, inv $ natCoefCoincide {b} {n} ) idp
+
+    {- | PreAdditiveCategory with one object is a ring -}
+    \func PreAdditiveCategory-OneObject (X : PreAdditivePrecat (\Sigma)) : Ring (X.Hom () ()) \cowith
+      | AbGroup => X.AbHom {()}{()}
+      | ide => X.id ()
+      | * => X.∘
+      | ide-left => X.id-left
+      | ide-right => X.id-right
+      | *-assoc => X.o-assoc
+      | ldistr => X.l-bilinear
+      | rdistr => X.r-bilinear
+
+    \func Ring_toCat (R : Ring) : PreAdditivePrecat (\Sigma) \cowith
+      | Hom () () => R
+      | id () => R.ide
+      | o => R.*
+      | id-left => R.ide-left
+      | id-right => R.ide-right
+      | o-assoc => R.*-assoc
+      | AbHom => R
+      | l-bilinear => R.ldistr
+      | r-bilinear => R.rdistr
+  }
+
+\class AdditivePrecat \extends PreAdditivePrecat, CartesianPrecat
\ No newline at end of file
diff --git a/src/Logic/Classical.ard b/src/Logic/Classical.ard
index 188855b6..fba5cb75 100644
--- a/src/Logic/Classical.ard
+++ b/src/Logic/Classical.ard
@@ -23,7 +23,7 @@
     \lemma lemFromChoice (P : \Prop) : Dec P
       => \let | R (x y : Bool) : \Prop => \case x, y \with {
                                        | true, true => \Sigma
-                                       | true, flase => P
+                                       | true, false => P
                                        | false, true => P
                                        | false, false => \Sigma
                                      }