\import Algebra.Field
\import Algebra.Group
\import Algebra.Group.GroupCategory
\import Algebra.Group.GroupHom
\import Algebra.Monoid
\import Algebra.Monoid.MonoidCategory
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Algebra.Pointed.PointedHom
\import Algebra.Ring
\import Algebra.Ring.RingCategory
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Category
\import Category.Functor
\import Function.Meta ($)
\import Logic
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.SetCategory
\open SetColimit

\instance MonoidLatticeColimit {D : BottomJoinSemilattice} (F : Functor D MonoidCat) : Monoid (SetColimit (Comp MonoidCat.forget F))
  | ide => in~ (D.bottom, ide)
  | * (x y : SetColimit (Comp MonoidCat.forget F)) : SetColimit (Comp MonoidCat.forget F) \with {
    | in~ a, in~ b => in~ (a. ∨ b., F.Func join-left a. Monoid.* F.Func join-right b.)
    | in~ a, ~-equiv x y r => ~-cequiv (D.join-monotone <=-refl r.) $ func-* *> pmap2 (Monoid.*) (inv Func-app *> poset-app)
                                                                                     (inv Func-app *> poset-app *> Func-app *> pmap (F.Func _) r.)
    | ~-equiv x y r, in~ b => ~-cequiv (D.join-monotone r. <=-refl) $ func-* *> pmap2 (Monoid.*)
                                                                                     (inv Func-app *> poset-app *> Func-app *> pmap (F.Func _) r.) (inv Func-app *> poset-app)
  }
  | ide-left {x} => \case \elim x \with {
    | in~ a => ~-cequiv (join-univ D.bottom-univ <=-refl) $ func-* *> pmap2 (Monoid.*) (pmap (F.Func _) func-ide *> func-ide) (inv Func-app *> poset-id) *> ide-left
  }
  | ide-right {x} => \case \elim x \with {
    | in~ a => ~-cequiv (join-univ <=-refl D.bottom-univ) $ func-* *> pmap2 (Monoid.*) (inv Func-app *> poset-id) (pmap (F.Func _) func-ide *> func-ide) *> ide-right
  }
  | *-assoc {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ a, in~ b, in~ c => ~-cequiv (=_<= D.join-assoc) $ func-* *> pmap2 (Monoid.*)
        (inv Func-app *> func-* *> pmap2 (Monoid.*) (inv Func-app *> poset-app) (inv Func-app *> poset-app *> Func-app))
        (inv Func-app *> poset-app *> Func-app) *> *-assoc *> pmap (_ Monoid.*) (inv func-*)
  }
  \where {
    \private \lemma Func-app {j1 j2 j3 : D} {f : Hom j1 j2} {g : Hom j2 j3} {a : F j1} : F.Func (g ∘ f) a = F.Func g (F.Func f a)
      => SetColimit.Func-app (Comp MonoidCat.forget F)

    \private \lemma poset-app {j j' : D} {f g : j <= j'} {a : F j} : F.Func f a = F.Func g a
      => pmap (F.Func __ a) prop-pi

    \private \lemma poset-id {j : D} {p : j <= j} {a : F j} : F.Func p a = a
      => SetColimit.poset-id {D} {Comp MonoidCat.forget F}

    \func inMap {F : Functor D MonoidCat} (d : D) : MonoidHom (F d) (MonoidLatticeColimit F) \cowith
      | func a => in~ (d,a)
      | func-ide => inv $ ~-cequiv D.bottom-univ func-ide
      | func-* => ~-cequiv join-left func-*

    \lemma inMap-coh {d d' : D} (p : d <= d') : inMap d = inMap d' ∘ F.Func p
      => exts \lam a => ~-cequiv p idp
  }

\instance AddMonoidLatticeColimit {D : BottomJoinSemilattice} (F : Functor D AddMonoidCat) : AddMonoid (SetColimit (Comp AddMonoidCat.forget F))
  | zro => in~ (D.bottom, zro)
  | + (x y : SetColimit (Comp AddMonoidCat.forget F)) : SetColimit (Comp AddMonoidCat.forget F) \with {
    | in~ a, in~ b => in~ (a. ∨ b., F.Func join-left a. AddMonoid.+ F.Func join-right b.)
    | in~ a, ~-equiv x y r => ~-cequiv (D.join-monotone <=-refl r.) $ func-+ *> pmap2 (AddMonoid.+) (inv Func-app *> poset-app)
        (inv Func-app *> poset-app *> Func-app *> pmap (F.Func _) r.)
    | ~-equiv x y r, in~ b => ~-cequiv (D.join-monotone r. <=-refl) $ func-+ *> pmap2 (AddMonoid.+)
        (inv Func-app *> poset-app *> Func-app *> pmap (F.Func _) r.) (inv Func-app *> poset-app)
  }
  | zro-left {x} => \case \elim x \with {
    | in~ a => ~-cequiv (join-univ D.bottom-univ <=-refl) $ func-+ *> pmap2 (AddMonoid.+) (pmap (F.Func _) func-zro *> func-zro) (inv Func-app *> poset-id) *> zro-left
  }
  | zro-right {x} => \case \elim x \with {
    | in~ a => ~-cequiv (join-univ <=-refl D.bottom-univ) $ func-+ *> pmap2 (AddMonoid.+) (inv Func-app *> poset-id) (pmap (F.Func _) func-zro *> func-zro) *> zro-right
  }
  | +-assoc {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ a, in~ b, in~ c => ~-cequiv (=_<= D.join-assoc) $ func-+ *> pmap2 (AddMonoid.+)
        (inv Func-app *> func-+ *> pmap2 (AddMonoid.+) (inv Func-app *> poset-app) (inv Func-app *> poset-app *> Func-app))
        (inv Func-app *> poset-app *> Func-app) *> +-assoc *> pmap (_ AddMonoid.+) (inv func-+)
  }
  \where {
    \private \lemma Func-app {j1 j2 j3 : D} {f : Hom j1 j2} {g : Hom j2 j3} {a : F j1} : F.Func (g ∘ f) a = F.Func g (F.Func f a)
      => SetColimit.Func-app (Comp AddMonoidCat.forget F)

    \private \lemma poset-app {j j' : D} {f g : j <= j'} {a : F j} : F.Func f a = F.Func g a
      => pmap (F.Func __ a) prop-pi

    \private \lemma poset-id {j : D} {p : j <= j} {a : F j} : F.Func p a = a
      => SetColimit.poset-id {D} {Comp AddMonoidCat.forget F}

    \func inMap {F : Functor D AddMonoidCat} (d : D) : AddMonoidHom (F d) (AddMonoidLatticeColimit F) \cowith
      | func a => in~ (d,a)
      | func-zro => inv $ ~-cequiv D.bottom-univ func-zro
      | func-+ => ~-cequiv join-left func-+

    \lemma inMap-coh {d d' : D} (p : d <= d') : inMap d = inMap d' ∘ F.Func p
      => exts \lam a => ~-cequiv p idp
  }

\instance AddGroupLatticeColimit {D : BottomJoinSemilattice} (F : Functor D AddGroupCat) : AddGroup (SetColimit (Comp AddGroupCat.forget F))
  | AddMonoid => AddMonoidLatticeColimit (Comp AddGroupCat.forgetToAddMonoid F)
  | negative (x : SetColimit (Comp AddGroupCat.forget F)) : SetColimit (Comp AddGroupCat.forget F) \with {
    | in~ a => in~ (a., AddGroup.negative a.)
    | ~-equiv x y r => ~-cequiv r. $ AddGroupHom.func-negative *> pmap AddGroup.negative r.
  }
  | negative-left {x} => \case \elim x \with {
    | in~ a => inv $ ~-cequiv D.bottom-univ $ func-zro *> inv func-zro *> pmap (F.Func _) (inv negative-left) *> func-+
  }
  | negative-right {x} => \case \elim x \with {
    | in~ a => inv $ ~-cequiv D.bottom-univ $ func-zro *> inv func-zro *> pmap (F.Func _) (inv negative-right) *> func-+
  } \where {
    \func inMap {F : Functor D AddGroupCat} (d : D) : AddGroupHom (F d) (AddGroupLatticeColimit F) \cowith
      | func a => in~ (d,a)
      | func-zro => inv $ ~-cequiv D.bottom-univ func-zro
      | func-+ => ~-cequiv join-left func-+

    \lemma inMap-coh {d d' : D} (p : d <= d') : inMap d = inMap d' ∘ F.Func p
      => exts \lam a => ~-cequiv p idp
  }

\instance AbGroupLatticeColimit {D : BottomJoinSemilattice} (F : Functor D AbGroupCat) : AbGroup (SetColimit (Comp AbGroupCat.forget F))
  | AddGroup => AddGroupLatticeColimit (Comp AbGroupCat.forgetToAddGroup F)
  | +-comm {x} {y} => \case \elim x, \elim y \with {
    | in~ a, in~ b => ~-cequiv (=_<= D.join-comm) $ func-+ *> +-comm *> pmap2 (+) (inv (Func-app (Comp AbGroupCat.forget F)) *> poset-app) (inv (Func-app (Comp AbGroupCat.forget F)) *> poset-app)
  }
  \where {
    \func inMap {F : Functor D AbGroupCat} (d : D) : AddGroupHom (F d) (AddGroupLatticeColimit F) \cowith
      | func a => in~ (d,a)
      | func-zro => inv $ ~-cequiv D.bottom-univ func-zro
      | func-+ => ~-cequiv join-left func-+

    \lemma inMap-coh {d d' : D} (p : d <= d') : inMap d = inMap d' ∘ F.Func p
      => exts \lam a => ~-cequiv p idp
  }

\instance RingLatticeColimit {D : BottomJoinSemilattice} (F : Functor D RingCat) : Ring (SetColimit (Comp RingCat.forget F))
  | AbGroup => AbGroupLatticeColimit (Comp RingCat.forgetToAbGroup F)
  | Monoid => MonoidLatticeColimit (Comp RingCat.forgetToMonoid F)
  | ldistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ a, in~ b, in~ c => ~-cequiv (join-univ (join-left <=∘ join-left) (D.join-monotone join-right join-right)) $
        pmap (\lam x => F.Func _ (_ * x)) func-+ *> pmap (F.Func _) ldistr *> func-+ *> pmap2 (+)
          (func-* *> pmap2 (*) (inv Func-app *> poset-app *> Func-app) (inv Func-app *> inv Func-app *> poset-app *> Func-app) *> inv func-*)
          (func-* *> pmap2 (*) (inv Func-app *> poset-app *> Func-app) (inv Func-app *> inv Func-app *> poset-app *> Func-app) *> inv func-*)
  }
  | rdistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ a, in~ b, in~ c => ~-cequiv (join-univ (D.join-monotone join-left join-left) (join-right <=∘ join-right)) $
        pmap (\lam x => F.Func _ (x * _)) func-+ *> pmap (F.Func _) rdistr *> func-+ *> pmap2 (+)
          (func-* *> pmap2 (*) (inv Func-app *> inv Func-app *> poset-app *> Func-app) (inv Func-app *> poset-app *> Func-app) *> inv func-*)
          (func-* *> pmap2 (*) (inv Func-app *> inv Func-app *> poset-app *> Func-app) (inv Func-app *> poset-app *> Func-app) *> inv func-*)
  }
  \where {
    \private \lemma Func-app {j1 j2 j3 : D} {f : Hom j1 j2} {g : Hom j2 j3} {a : F j1} : F.Func (g ∘ f) a = F.Func g (F.Func f a)
      => SetColimit.Func-app (Comp RingCat.forget F)

    \private \lemma poset-app {j j' : D} {f g : j <= j'} {a : F j} : F.Func f a = F.Func g a
      => pmap (F.Func __ a) prop-pi

    \func inMap (d : D) : RingHom (F d) (RingLatticeColimit F) \cowith
      | func a => in~ (d,a)
      | func-zro => inv $ ~-cequiv D.bottom-univ func-zro
      | func-+ => ~-cequiv join-left func-+
      | func-ide => inv $ ~-cequiv D.bottom-univ func-ide
      | func-* => ~-cequiv join-left func-*

    \lemma inMap-coh {d d' : D} (p : d <= d') : inMap d = inMap d' ∘ F.Func p
      => exts \lam a => ~-cequiv p idp
  }

\instance CRingLatticeColimit {D : BottomJoinSemilattice} (F : Functor D CRingCat) : CRing (SetColimit (Comp CRingCat.forget F))
  | Ring => RingLatticeColimit (Comp CRingCat.forgetToRing F)
  | *-comm {x} {y} => \case \elim x, \elim y \with {
    | in~ a, in~ b => ~-cequiv (=_<= D.join-comm) $ func-* *> *-comm *> pmap2 (*) (inv (Func-app (Comp CRingCat.forget F)) *> poset-app) (inv (Func-app (Comp CRingCat.forget F)) *> poset-app)
  }

\func DiscreteFieldLatticeColimit {D : BottomJoinSemilattice} (F : Functor D CRingCat) (p : \Pi (d : D) -> DiscreteField { | CRing => F d }) : DiscreteField (SetColimit (Comp CRingCat.forget F)) \cowith
  | CRing => CRingLatticeColimit F
  | zro/=ide q => \case unext-ub q \with {
    | inP s => zro/=ide {p s.} $ inv func-zro *> s. *> func-ide
  }
  | eitherZeroOrInv (in~ x) => \case eitherZeroOrInv {p x.} x. \with {
    | byLeft r => byLeft $ inv $ ~-cequiv D.bottom-univ $ func-zro *> inv r
    | byRight (r : Monoid.Inv) => byRight $ Monoid.Inv.lmake (inC (x., r.inv)) $ later $ inv $ ~-cequiv D.bottom-univ $ func-ide *> inv (pmap (F.Func _) r.inv-left *> func-ide) *> func-*
  }