Category

\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Category
\import Category.Adjoint
\import Category.Functor
\import Category.Limit
\import Category.Meta
\import Equiv (QEquiv)
\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

\record MonoidHom \extends PointedHom {
  \override Dom : Monoid
  \override Cod : Monoid
  | func-* {x y : Dom} : func (x * y) = func x * func y

  \lemma func-pow {x : Dom} {n : Nat} : func (Monoid.pow x n) = Monoid.pow (func x) n \elim n
    | 0 => func-ide
    | suc n => func-* *> pmap (`* _) func-pow

  \lemma func-BigProd {l : Array Dom} : func (Monoid.BigProd l) = Monoid.BigProd (\lam j => func (l j)) \elim l
    | nil => func-ide
    | a :: l => func-* *> pmap (_ *) func-BigProd

  \lemma func-LDiv {a b : Dom} (d : Monoid.LDiv a b) : Monoid.LDiv (func a) (func b) (func d.inv) \cowith
    | inv-right => inv func-* *> pmap func d.inv-right

  \lemma func-Inv {a : Dom} (d : Monoid.Inv a) : Monoid.Inv (func a) (func d.inv) \cowith
    | inv-left => inv func-* *> pmap func d.inv-left *> func-ide
    | inv-right => inv func-* *> pmap func d.inv-right *> func-ide
}
  \where {
    \func equals {M N : Monoid} {f g : MonoidHom M N} (p : \Pi (x : M) -> f x = g x) : f = g
      => exts p

    \open Monoid(Inv)

    \func presInv (h : MonoidHom) (e : Inv {h.Dom}) : Inv (h e) \cowith
      | inv => h e.inv
      | inv-left => inv h.func-* *> pmap h e.inv-left *> h.func-ide
      | inv-right => inv h.func-* *> pmap h e.inv-right *> h.func-ide

    \lemma presInvElem (h : MonoidHom) (e : Inv {h.Dom}) (e' : Inv (h e)) : h e.inv = e'.inv
      => pmap (\lam (j : Inv) => j.inv) (Inv.levelProp (\new Inv (h e) {
        | inv => h e.inv
        | inv-left => inv h.func-* *> pmap h e.inv-left *> h.func-ide
        | inv-right => inv h.func-* *> pmap h e.inv-right *> h.func-ide
      }) e')

    \lemma func-inverse {G H : Group} (h : MonoidHom G H) {a : G} : h (inverse a) = inverse (h a)
      => presInvElem h (G.makeInv a) (H.makeInv (h a))
  }

\instance MonoidCat : Cat Monoid
  | Hom M N => MonoidHom M N
  | id => id
  | o {x y z : Monoid} (g : MonoidHom y z) (f : MonoidHom x y) => \new MonoidHom {
    | func x => g (f x)
    | func-ide => pmap g f.func-ide *> g.func-ide
    | func-* => pmap g f.func-* *> g.func-*
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam p1 p2 => exts (func-ide {p1}, \lam _ _ => func-* {p1}))
  \where {
    \func id (M : Monoid) : MonoidHom M M \cowith
      | func x => x
      | func-ide => idp
      | func-* => idp

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

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

    \func catEquiv : CatEquiv (ModelCat theory) MonoidCat modToMonoid \cowith
      | Func (f : ModelHom) => \new MonoidHom {
        | func => f.funcs
        | func-ide => f.func-op 0 nil
        | func-* {x} {y} => f.func-op 1 (x :: y :: nil)
      }
      | Func-id => idp
      | Func-o => idp
      | LAdj => monoidToMod.functor
      | eta {
        | trans M => id M
        | natural f => idp
      }
      | isAdjoint => \new QEquiv {
        | ret (h : MonoidHom) => \new ModelHom {
          | funcs => h
          | func-op => \case \elim __ \with {
            | 0 => \lam _ => h.func-ide
            | 1 => \lam d => h.func-*
          }
          | 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
          }
          | func-rel => \case __
        }
        | hinv_f => idp
        | f_hinv => idp
      }

    \func modToMonoid (M : Model theory) : Monoid (M ()) \cowith
      | ide => operation 0 nil
      | * x y => operation 1 (x :: y :: nil)
      | ide-left {x} => M.isModel _ (inP (0,idp)) (\lam _ => x) (\case __)
      | ide-right {x} => M.isModel _ (inP (1,idp)) (\lam _ => x) (\case __)
      | *-assoc {x} {y} {z} => M.isModel _ (inP (2,idp)) (\lam {_} => x :: y :: z :: nil) (\case __)

    \func monoidToMod (M : Monoid) : Model theory (\lam _ => M) \cowith
      | operation => \case \elim __ \with {
        | 0 => \lam _ => ide
        | 1 => \lam l => l 0 * l 1
      }
      | relation => \case __
      | isModel => \case \elim __, __ \with {
        | _, inP (0,idp) => \lam rho _ => ide-left
        | _, inP (1,idp) => \lam rho _ => ide-right
        | _, inP (2,idp) => \lam rho _ => *-assoc
      }
      \where {
        \func functor : Functor MonoidCat (ModelCat theory) monoidToMod \cowith
          | Func (f : MonoidHom) => \new ModelHom {
            | funcs => f
            | func-op => \case \elim __ \with {
              | 0 => \lam _ => f.func-ide
              | 1 => \lam d => f.func-*
            }
            | func-rel => \case __
          }
          | Func-id => idp
          | Func-o => idp
      }
  }

\record AddMonoidHom \extends AddPointedHom {
  \override Dom : AddMonoid
  \override Cod : AddMonoid
  | func-+ {x y : Dom} : func (x + y) = func x + func y

  \lemma func-BigSum {l : Array Dom} : func (AddMonoid.BigSum l) = AddMonoid.BigSum (\lam j => func (l j)) \elim l
    | nil => func-zro
    | a :: l => func-+ *> pmap (_ +) func-BigSum
} \where {
  \use \coerce toMonoidHom (f : AddMonoidHom) : MonoidHom \cowith
    | Dom => f.Dom
    | Cod => f.Cod
    | func => f
    | func-* => func-+
    | func-ide => func-zro

  \lemma func-FinSum {A B : AbMonoid} (f : AddMonoidHom A B) {J : FinSet} {a : J -> A} : f (A.FinSum a) = B.FinSum (\lam j => f (a j))
    => \case A.FinSum_char a \with {
         | inP (e,q) => pmap f q *> func-BigSum *> inv (B.FinSum_char2 _ e)
       }
}

\instance AddMonoidCat : Cat AddMonoid
  | Hom M N => AddMonoidHom M N
  | id => id
  | o g f => \new AddMonoidHom {
    | func x => g (f x)
    | func-zro => pmap g func-zro *> func-zro
    | func-+ => pmap g func-+ *> func-+
  }
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => sip (\lam {X} {A} {B} (p1 : AddMonoidHom) p2 => exts (p1.func-zro, \lam _ _ => p1.func-+))
  \where {
    \func id (M : AddMonoid) : AddMonoidHom M M \cowith
      | func x => x
      | func-zro => idp
      | func-+ => idp

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

\instance KerAddMonoid (f : AddMonoidHom) : AddMonoid
  | AddPointed => KerAddPointed f
  | + a b => (a.1 + b.1, func-+ *> pmap2 (+) a.2 b.2 *> zro-left)
  | zro-left => ext zro-left
  | zro-right => ext zro-right
  | +-assoc => ext +-assoc

\func KerMonoidHom (f : AddMonoidHom) : AddMonoidHom (KerAddMonoid f) f.Dom \cowith
  | AddPointedHom => KerPointedHom f
  | func-+ => idp

\instance KerAbMonoid {A : AbMonoid} (f : AddMonoidHom A) : AbMonoid (Kernel f)
  | AddMonoid => KerAddMonoid f
  | +-comm => ext +-comm

\instance ImageAddMonoid (f : AddMonoidHom) : AddMonoid
  | AddPointed => ImageAddPointed f
  | + a b => (a.1 + b.1, \case a.2, b.2 \with {
    | inP t, inP s => inP (t.1 + s.1, func-+ *> pmap2 (+) t.2 s.2)
  })
  | zro-left => ext zro-left
  | zro-right => ext zro-right
  | +-assoc => ext +-assoc

\instance ImageMonoid (f : MonoidHom) : Monoid
  | Pointed => ImageMulPointed f
  | * a b => (a.1 * b.1, \case a.2, b.2 \with {
    | inP t, inP s => inP (t.1 * s.1, func-* *> pmap2 (*) t.2 s.2)
  })
  | ide-left => ext ide-left
  | ide-right => ext ide-right
  | *-assoc => ext *-assoc

\func ImageMonoidLeftHom (f : AddMonoidHom) : AddMonoidHom f.Dom (ImageAddMonoid f) \cowith
  | AddPointedHom => ImagePointedLeftHom f
  | func-+ => ext func-+

\func ImageMonoidRightHom (f : AddMonoidHom) : AddMonoidHom (ImageAddMonoid f) f.Cod \cowith
  | AddPointedHom => ImagePointedRightHom f
  | func-+ => idp

\instance ImageAbMonoid {A : AddMonoid} {B : AbMonoid} (f : AddMonoidHom A B) : AbMonoid
  | AddMonoid => ImageAddMonoid f
  | +-comm => ext +-comm