\import Algebra.Group
\import Algebra.Group.GroupCategory
\import Algebra.Group.GroupHom
\import Algebra.Monoid
\import Algebra.Monoid.MonoidCategory
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Ring.Sub
\import Algebra.Semiring
\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Limit
\import Category.Meta
\import Category.Subcat
\import Equiv
\import Function (IsInj, IsSurj)
\import Function.Meta
\import Logic
\import Logic.FirstOrder.Algebraic
\import Logic.FirstOrder.Algebraic.Category
\import Logic.FirstOrder.Term
\import Paths
\import Paths.Meta
\import Set.SetCategory
\import Set.Fin
\import Set.Fin.Instances

\instance RingCat : Cat Ring
  | Hom M N => RingHom M N
  | id _ => RingHom.id
  | o => RingHom.∘
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {R} {S} (p1 : RingHom) _ => exts (p1.func-zro, \lam _ _ => p1.func-+, \lam _ _ => p1.func-*, AddGroup.negative-equality R S p1.func-zro p1.func-+, p1.func-ide, natCoefUnique R S p1))
  \where {
    \lemma natCoefUnique {X : \Set} (R S : Ring X) (h : RingHom R S (\lam x => x)) (n : Nat) : R.natCoef n = S.natCoef n \elim n
      |  => R.natCoefZero *> h.func-zro *> inv S.natCoefZero
      | suc n => R.natCoefSuc n *> h.func-+ *> pmap2 (S.+) (natCoefUnique R S h n) h.func-ide *> inv (S.natCoefSuc n)

    \func forgetToAbGroup : Functor RingCat AbGroupCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forgetToMonoid : Functor RingCat MonoidCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forget : Functor RingCat SetCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    {- | A function that lifts an isomorphism between the additive groups of two rings
         to an isomorphism between the rings themselves**. `Group-Iso->Ring-Iso` -}
    \lemma Group-Iso->Ring-Iso {G H : Ring} {f : RingHom G H} (f_iso : Iso {GroupCat} (AddGroupHom.toGroupHom f)) : Iso {RingCat} f \cowith {
      | hinv => \new RingHom {
        | AddGroupHom => AddGroupHom.fromGroupHom f_iso.hinv
        | func-ide => rewrite (inv f.func-ide, path \lam i => f_iso.hinv_f i ide) idp
        | func-* {x} {y} =>
          \let | x' => f_iso.hinv x
               | y' => f_iso.hinv y
          \in rewrite (inv $ path \lam i => f_iso.f_hinv i x,
                       inv $ path \lam i => f_iso.f_hinv i y,
                       inv f.func-*,
                       path \lam i => f_iso.hinv_f i y',
                       path \lam i => f_iso.hinv_f i x') $
              path \lam i => f_iso.hinv_f i _
      }
      | hinv_f => exts \lam e i => f_iso.hinv_f i e
      | f_hinv => exts \lam e i => f_iso.f_hinv i e
    }

    \lemma Iso<->Inj+Surj {G H : Ring} (f : RingHom G H) : Iso {RingCat} f <-> (\Sigma (IsInj f) (IsSurj f)) =>
      (\lam p => (GroupCat.Iso<->Inj+Surj (AddGroupHom.toGroupHom f)). \new Iso {
        | hinv => AddGroupHom.toGroupHom hinv
        | hinv_f => exts \lam e i => p.hinv_f i e
        | f_hinv => exts \lam e i => p.f_hinv i e
      }, \lam p => Group-Iso->Ring-Iso ((GroupCat.Iso<->Inj+Surj (AddGroupHom.toGroupHom f)). p))

    \func image-iso {f : RingHom} (p : IsSurj f) : Iso {RingCat} {f.Image.IRing} {f.Cod}
      => (RingCat.Iso<->Inj+Surj f.image). (RingHom.image.isInj, RingHom.image.isSurj p)

    \func Image=Cod {R S : Ring} (f : RingHom R S) (p : IsSurj f) : (ringHomImage f).IRing = {Ring} S
      => RingCat.isotoid (image-iso p)
  }

\instance CRingCat : Cat CRing
=> subCat (\new Embedding {CRing} {Ring} {
  | f R => R
  | isEmb (R S : CRing) => \new Retraction {
    | sec p => path (\lam i => \new CRing {
      | Ring => p @ i
      | *-comm => prop-dpi (\Pi {x y : p @ __} -> x * y = y * x) R.*-comm S.*-comm @ i
    })
    | f_sec => idpe
  }
})
  \where {
    \func forgetToRing : Functor CRingCat RingCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp

    \func forget : Functor CRingCat SetCat \cowith
      | F R => R
      | Func f => f
      | Func-id => idp
      | Func-o => idp
      \where {
        \func reflectsLimit {J : SmallPrecat} (H : Functor J CRingCat) : ReflectsLimit forget H
          => (CRingBicat.createsLimits H (SetBicat.limit (Comp CRingCat.forget H))).

        \func preservesLimit {J : SmallPrecat} (H : Functor J CRingCat) : PreservesLimit forget H
          => (CRingBicat.createsLimits H (SetBicat.limit (Comp CRingCat.forget H))).
      }

    \func Image=Cod {R : Ring} {S : CRing} (f : RingHom R S) (p : IsSurj f) : (RingHom.ImageC f).ICRing = {CRing} S
      => ext CRing { | Ring => RingCat.Image=Cod f p }
  }

\instance CRingBicat : BicompleteCat
  | Cat => CRingCat
  | limit => CompletePrecat.applyEquiv catEquiv
  | colimit => CocompletePrecat.applyEquiv catEquiv
  \where {
    \instance theory : Theory
      | Sort => \Sigma
      | Symb _ => Fin 
      | domain => \case __ \with {
        |  => nil
        |  => nil
        |  => () :: () :: nil
        |  => () :: () :: nil
        |  => () :: nil
      }
      | PredSymb => Empty
      | predDomain => absurd
      | axioms => arraySubset {Sequent {\this}} (
          (\lam _ => \Sigma, finSet, nil, equality (apply  (apply  nil :: var () :: nil)) (var ())) ::
          (\lam _ => Fin ,  finSet, nil, equality (apply  (apply  (var  :: var  :: nil) :: var  :: nil)) (apply  (var  :: apply  (var  :: var  :: nil) :: nil))) ::
          (\lam _ => \Sigma, finSet, nil, equality (apply  (apply  nil :: var () :: nil)) (var ())) ::
          (\lam _ => Fin ,  finSet, nil, equality (apply  (apply  (var  :: var  :: nil) :: var  :: nil)) (apply  (var  :: apply  (var  :: var  :: nil) :: nil))) ::
          (\lam _ => Fin ,  finSet, nil, equality (apply  (var  :: var  :: nil)) (apply  (var  :: var  :: nil))) ::
          (\lam _ => Fin ,  finSet, nil, equality (apply  (var  :: var  :: nil)) (apply  (var  :: var  :: nil))) ::
          (\lam _ => \Sigma, finSet, nil, equality (apply  (apply  (var () :: nil) :: var () :: nil)) (apply  nil)) ::
          (\lam _ => Fin ,  finSet, nil, equality (apply  (var  :: apply  (var  :: var  :: nil) :: nil)) (apply  (apply  (var  :: var  :: nil) :: apply  (var  :: var  :: nil) :: nil))) ::
          nil)

    \func catEquiv : CatEquiv (ModelCat theory) CRingCat modToRing \cowith
      | Func (f : ModelHom) => \new RingHom {
        | func => f.funcs
        | func-zro => f.func-op  nil
        | func-ide => f.func-op  nil
        | func-+ {x} {y} => f.func-op  (x :: y :: nil)
        | func-* {x} {y} => f.func-op  (x :: y :: nil)
      }
      | Func-id => idp
      | Func-o => idp
      | LAdj => ringtoMod.functor
      | eta {
        | trans M => id M
        | natural f => idp
      }
      | eta-iso {X} => \new Iso {
        | hinv => id X
        | hinv_f => idp
        | f_hinv => idp
      }
      | epsilon {
        | trans M => \new ModelHom {
          | funcs x => x
          | func-op => \case \elim __ \with {
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
          }
          | func-rel => \case __
        }
        | natural f => idp
      }
      | eta_epsilon-left => idp
      | eta_epsilon-right => idp
      | epsilon-iso {Y} => \new Iso {
        | hinv => \new ModelHom {
          | funcs y => y
          | func-op => \case \elim __ \with {
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
            |  => \lam d => idp
          }
          | func-rel => \case __
        }
        | hinv_f => idp
        | f_hinv => idp
      }

    \func modToRing (M : Model theory) : CRing (M ()) \cowith
      | zro => operation  nil
      | ide => operation  nil
      | + x y => operation  (x :: y :: nil)
      | * x y => operation  (x :: y :: nil)
      | negative x => operation  (x :: nil)
      | zro-left {x} => M.isModel _ (inP (,idp)) (\lam _ => x) (\case __)
      | +-assoc {x} {y} {z} => M.isModel _ (inP (,idp)) (\lam {_} => x :: y :: z :: nil) (\case __)
      | ide-left {x} => M.isModel _ (inP (,idp)) (\lam _ => x) (\case __)
      | *-assoc {x} {y} {z} => M.isModel _ (inP (,idp)) (\lam {_} => x :: y :: z :: nil) (\case __)
      | +-comm {x} {y} => M.isModel _ (inP (,idp)) (\lam {_} => x :: y :: nil) (\case __)
      | *-comm {x} {y} => M.isModel _ (inP (,idp)) (\lam {_} => x :: y :: nil) (\case __)
      | negative-left {x} => M.isModel _ (inP (,idp)) (\lam {_} _ => x) (\case __)
      | ldistr {x} {y} {z} => M.isModel _ (inP (,idp)) (\lam {_} => x :: y :: z :: nil) (\case __)

    \func ringtoMod (R : CRing) : Model theory (\lam _ => R) \cowith
      | operation => \case \elim __ \with {
        |  => \lam _ => 
        |  => \lam _ => 
        |  => \lam l => l  + l 
        |  => \lam l => l  * l 
        |  => \lam l => negative (l )
      }
      | relation => \case __
      | isModel => \case \elim __, __ \with {
        | _, inP (,idp) => \lam rho _ => zro-left
        | _, inP (,idp) => \lam rho _ => +-assoc
        | _, inP (,idp) => \lam rho _ => ide-left
        | _, inP (,idp) => \lam rho _ => *-assoc
        | _, inP (,idp) => \lam rho _ => +-comm
        | _, inP (,idp) => \lam rho _ => *-comm
        | _, inP (,idp) => \lam rho _ => negative-left
        | _, inP (,idp) => \lam rho _ => ldistr
      }
      \where {
        \func functor : Functor CRingCat (ModelCat theory) ringtoMod \cowith
          | Func (f : RingHom) => \new ModelHom {
            | funcs => f
            | func-op => \case \elim __ \with {
              |  => \lam _ => f.func-zro
              |  => \lam _ => f.func-ide
              |  => \lam _ => f.func-+
              |  => \lam _ => f.func-*
              |  => \lam _ => f.func-negative
            }
            | func-rel => \case __
          }
          | Func-id => idp
          | Func-o => idp
      }

    \sfunc createsLimits {J : SmallPrecat} (F : Functor J CRingCat) : CreatesLimit CRingCat.forget F
      => {?}
  }