\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, \lam _ _ => idp, \lam _ => idp, idp, \lam n => natCoefCoincide)
}
  \where {
    \func natCoefCoincide {b : Ring}{n : Nat} : natCoef {PreAdditiveCategory-OneObject (Ring_toCat b)} n = b.natCoef n \elim n
      |  => 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