\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
    |  => 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

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

    \func catEquiv : CatEquiv (ModelCat theory) MonoidCat modToMonoid \cowith
      | Func (f : ModelHom) => \new MonoidHom {
        | func => f.funcs
        | func-ide => f.func-op  nil
        | func-* {x} {y} => f.func-op  (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 {
            |  => \lam _ => h.func-ide
            |  => \lam d => h.func-*
          }
          | 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
          }
          | func-rel => \case \elim __
        }
        | inv_f => idp
        | f_inv => idp
      }

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

    \func monoidToMod (M : Monoid) : Model theory (\lam _ => M) \cowith
      | operation => \case \elim __ \with {
        |  => \lam _ => ide
        |  => \lam l => l  * l 
      }
      | relation => \case __
      | isModel => \case \elim __, \elim __ \with {
        | _, inP (,idp) => \lam rho _ => ide-left
        | _, inP (,idp) => \lam rho _ => ide-right
        | _, inP (,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 {
              |  => \lam _ => f.func-ide
              |  => \lam d => f.func-*
            }
            | func-rel => \case __
          }
          | Func-id => idp
          | Func-o => idp
      }
  }