Category

\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Monoid
\import Algebra.Monoid.Category
\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
\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
      | 0 => 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 => func {f}
      | Func-id => idp
      | Func-o => idp
  }

\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 => func {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))).3

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

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

    \func catEquiv : CatEquiv (ModelCat theory) CRingCat modToRing \cowith
      | Func (f : ModelHom) => \new RingHom {
        | func => f.funcs
        | func-zro => f.func-op 0 nil
        | func-ide => f.func-op 1 nil
        | func-+ {x} {y} => f.func-op 2 (x :: y :: nil)
        | func-* {x} {y} => f.func-op 3 (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 {
            | 0 => \lam _ => h.func-zro
            | 1 => \lam _ => h.func-ide
            | 2 => \lam d => h.func-+
            | 3 => \lam d => h.func-*
            | 4 => \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 {
        | hinv => id X
        | hinv_f => idp
        | f_hinv => idp
      }
      | epsilon-iso {Y} => \new Iso {
        | hinv => \new ModelHom {
          | funcs y => y
          | func-op => \case \elim __ \with {
            | 0 => \lam d => idp
            | 1 => \lam d => idp
            | 2 => \lam d => idp
            | 3 => \lam d => idp
            | 4 => \lam d => idp
          }
          | func-rel => \case __
        }
        | hinv_f => idp
        | f_hinv => idp
      }

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

    \func ringtoMod (R : CRing) : Model theory (\lam _ => R) \cowith
      | operation => \case \elim __ \with {
        | 0 => \lam _ => 0
        | 1 => \lam _ => 1
        | 2 => \lam l => l 0 + l 1
        | 3 => \lam l => l 0 * l 1
        | 4 => \lam l => negative (l 0)
      }
      | relation => \case __
      | isModel => \case \elim __, __ \with {
        | _, inP (0,idp) => \lam rho _ => zro-left
        | _, inP (1,idp) => \lam rho _ => +-assoc
        | _, inP (2,idp) => \lam rho _ => ide-left
        | _, inP (3,idp) => \lam rho _ => *-assoc
        | _, inP (4,idp) => \lam rho _ => +-comm
        | _, inP (5,idp) => \lam rho _ => *-comm
        | _, inP (6,idp) => \lam rho _ => negative-left
        | _, inP (7,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 {
              | 0 => \lam _ => f.func-zro
              | 1 => \lam _ => f.func-ide
              | 2 => \lam _ => f.func-+
              | 3 => \lam _ => f.func-*
              | 4 => \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
      => {?}
  }