\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Limit
\import Category.Meta
\import Category.Subcat
\import Equiv \hiding (Map)
\import Logic
\import Logic.FirstOrder.Algebraic
\import Logic.FirstOrder.Algebraic.Category
\import Logic.FirstOrder.Term
\import Paths
\import Paths.Meta
\import Set.Category
\import Set.Fin

\instance RingCat : Cat Ring
  | Hom M N => RingHom M N
  | id => id
  | o {x y z : Ring} (g : RingHom y z) (f : RingHom x y) => \new RingHom {
    | func x => g (f x)
    | func-ide => pmap g f.func-ide *> g.func-ide
    | func-+ => pmap g f.func-+ *> g.func-+
    | func-* => pmap g f.func-* *> g.func-*
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {R} {S} (p1 : RingHom) _ => exts (p1.func-zro, \lam _ _ => p1.func-+, p1.func-ide, \lam _ _ => p1.func-*, natCoefUnique R S p1, AddGroup.negative-equality R S p1.func-zro p1.func-+))
  \where {
    \func id (M : Ring) : RingHom M M \cowith
      | func x => x
      | func-ide => idp
      | func-+ => idp
      | func-* => idp

    \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)
  }

\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 => pathInProp (\Pi {x y : p @ __} -> x * y = y * x) R.*-comm S.*-comm @ i
    })
    | f_sec => idpe
  }
})
  \where {
    \func forgetful : Functor CRingCat SetCat \cowith
      | F R => R
      | Func f => func {f}
      | Func-id => idp
      | Func-o => idp
      \where {
        \func reflectsLimit {J : SmallPrecat} (H : Functor J CRingCat) : ReflectsLimit forgetful H
          => (CRingBicat.createsLimits H (SetBicat.limit (Comp CRingCat.forgetful H))).

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

\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, _, nil, equality (apply  (apply  nil :: var () :: nil)) (var ())) ::
          (\lam _ => Fin ,  _, nil, equality (apply  (apply  (var  :: var  :: nil) :: var  :: nil)) (apply  (var  :: apply  (var  :: var  :: nil) :: nil))) ::
          (\lam _ => \Sigma, _, nil, equality (apply  (apply  nil :: var () :: nil)) (var ())) ::
          (\lam _ => Fin ,  _, nil, equality (apply  (apply  (var  :: var  :: nil) :: var  :: nil)) (apply  (var  :: apply  (var  :: var  :: nil) :: nil))) ::
          (\lam _ => Fin ,  _, nil, equality (apply  (var  :: var  :: nil)) (apply  (var  :: var  :: nil))) ::
          (\lam _ => Fin ,  _, nil, equality (apply  (var  :: var  :: nil)) (apply  (var  :: var  :: nil))) ::
          (\lam _ => \Sigma,  _, nil, equality (apply  (apply  (var () :: nil) :: var () :: nil)) (apply  nil)) ::
          (\lam _ => Fin ,  _, 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
      }
      | isAdjoint => \new QEquiv {
        | ret (h : RingHom) => \new ModelHom {
          | funcs => h
          | func-op => \case \elim __ \with {
            |  => \lam _ => h.func-zro
            |  => \lam _ => h.func-ide
            |  => \lam d => h.func-+
            |  => \lam d => h.func-*
            |  => \lam d => h.func-negative
          }
          | func-rel => \case __
        }
        | ret_f X => path (\lam _ => X)
        | f_sec X => path (\lam _ => X)
      }
      | eta-iso {X} => \new Iso {
        | inv => id X
        | inv_f => idp
        | f_inv => idp
      }
      | epsilon-iso {Y} => \new Iso {
        | inv => \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 \elim __
        }
        | inv_f => idp
        | f_inv => 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 __, \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.forgetful F
      => {?}
  }