\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Paths.Meta

\instance ProductCRing (R S : CRing) : CRing (\Sigma R S)
  | zro => (R.zro, S.zro)
  | + s t => (s. R.+ t., s. S.+ t.)
  | +-assoc => ext (R.+-assoc, S.+-assoc)
  | +-comm => ext (R.+-comm, S.+-comm)
  | * s t => (s. R.* t., s. S.* t.)
  | *-assoc => ext (R.*-assoc, S.*-assoc)
  | negative s => (R.negative s., S.negative s.)
  | negative-left => ext (R.negative-left, S.negative-left)
  | ide => (R.ide, S.ide)
  | *-comm => ext (R.*-comm, S.*-comm)
  | ide-left => ext (R.ide-left, S.ide-left)
  | ldistr => ext (R.ldistr, S.ldistr)
  | zro-left => ext (R.zro-left, S.zro-left)
  \where {
    \func proj1 : RingHom (ProductCRing R S) R \cowith
      | func s => s.
      | func-+ => idp
      | func-* => idp
      | func-ide => idp

    \func proj2 : RingHom (ProductCRing R S) S \cowith
      | func s => s.
      | func-+ => idp
      | func-* => idp
      | func-ide => idp
  }