\import Algebra.Group
\import Algebra.Group.Representation.Category
\import Algebra.Group.Representation
\import Algebra.Meta
\import Algebra.Module
\import Algebra.Module.LinearMap
\import Algebra.Pointed
\import Algebra.Ring
\import Function.Meta
\import Paths
\import Paths.Meta

\func ProductLRepres {R : Ring} {G : Group} (A B : LinRepres R G) : LinRepres 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 : LinRepres R G) : InterwiningMap A (ProductLRepres A B) \cowith
      | func a => (a, )
      | 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 : LinRepres R G) : InterwiningMap B (ProductLRepres A B) \cowith
      | func b => (, 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 : LinRepres 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 : LinRepres 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 : LinRepres 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
  }