\import Function.Meta
\import Homotopy.Loop
\import Homotopy.Pointed \using  (Pointed \as HPointed)
\import Meta
\import Paths
\import Paths.Meta

{- | This is an algebraic formulation of Eckmann Hilton argument.
 - It is used, for example, to prove that a monoid object in category of monoids is commutative
 - -}
\class Algebraic-Eckmann-Hilton (X : \Type) {
  | \infix  o : X -> X -> X
  | \infix  # : X -> X -> X
  | id_o : X
  | id_o-left {x : X} : id_o o x = x
  | id_o-right {x : X} : x o id_o = x

  | id_# : X
  | id_#-left {x : X} : id_# # x = x
  | id_#-right {x : X} : x # id_# = x

  | rel {a b c d : X} : (a # b) o (c # d) = (a o c) # (b o d)

  \func units-coincide : id_o = id_#
    => rewrite (inv id_o-right, pmap (id_o o) (inv $ id_#-left),
                pmap (o (id_# # id_o)) (inv $ id_#-right), rel, id_o-left, id_o-right) id_#-right

  \func binop_rels_1 {a b : X} : a o b = b # a
    => rewrite (pmap (\lam z => z o b) (inv id_#-left),
                pmap (\lam z => (id_# # a) o z) (inv id_#-right), rel, inv units-coincide,
                id_o-left, id_o-right) idp

  \func binop_rels_2 {a b : X} : b # a = b o a
    => rewrite (pmap (\lam z => z # a) (inv id_o-right),
                pmap (\lam z => (b o id_o) # z) (inv id_o-left), inv rel,
                units-coincide, id_#-right, id_#-left) idp

  \func comm {a b : X} : a o b = b o a => binop_rels_1 *> binop_rels_2

  \func binops_coincide {a b : X} : a o b = a # b => comm *> binop_rels_1

  \func comm-# {a b : X} : a # b = b # a => rewrite (inv binops_coincide, binop_rels_1) idp

  \func rel-o {a b c d : X} : (a o b) o (c o d) = (a o c) o (b o d) =>
    rewrite (binops_coincide {_} {a} {b}, binops_coincide {_} {c} {d}, rel, inv binops_coincide) idp

  \func assoc {a b c : X} : (a o b) o c = a o (b o c)
    => rewrite (inv $ id_o-left {_} {c}, rel-o, id_o-left, id_o-right) idp
}

\func RightHorizontalWhiskering {X : \Type} {a b c : X} {p q : a = b} (alp : p = q) (r : b = c) : p *> r = q *> r
  => path (\lam i => alp i *> r)

\func LeftHorizontalWhiskering {X : \Type} {a b c : X} (q : a = b) {r s : b = c} (bet : r = s) : q *> r = q *> s
  => path (\lam i => q *> bet i)

{- | This is the proof that Omega^2 X given the composition structure
 - forms a commutative monoid. This proof follows the proof from the HoTT Book
 - It has some minor changes that are possible with Arend features.
 - -}
\class Omega^2-Commutative (X : HPointed) {
  \func Omega^2_X => Loop (Loop X)

  \func LeftHorizontalWhiskering-relation {b c : X} {r s : b = c} (bet : r = s)
    : LeftHorizontalWhiskering (idp {X} {b}) bet = idp_*> r *> bet *> inv (idp_*> s) \elim bet
    | idp => unfold LeftHorizontalWhiskering (rewrite (inv $ *>-assoc (idp_*> r) idp (inv (idp_*> r)), aux) idp)
    \where {
      \protected \func aux {f : b = c} : idp_*> f *> inv (idp_*> f) = idp \elim f
        | idp => idp
    }

  \protected \func \infix  st1 {a b c : X} {p q : a = b} {r s : b = c} (alp : p = q) (bet : r = s) : p *> r = q *> s
    => RightHorizontalWhiskering alp r *> LeftHorizontalWhiskering q bet

  \protected \func \infix  st2 {a b c : X} {p q : a = b} {r s : b = c} (alp : p = q) (bet : r = s) : p *> r = q *> s
    => LeftHorizontalWhiskering p bet *> RightHorizontalWhiskering alp s

  \protected \func Relation {a b c : X} {p q : a = b} {r s : b = c} (alp : p = q) (bet : r = s) : alp st1 bet = alp st2 bet \elim alp, bet
    | idp, idp => helper
    \where {
      \protected \func helper {a b c : X} {p : a = b} {r : b = c} : idpe p st1 idpe r = idpe p st2 idpe r \elim p, r
        | idp, idp => idp
    }

  \protected \func Commutative (alp bet : Omega^2_X) : alp *> bet = bet *> alp => rewrite (inv Relation1, Relation3, Relation2) idp
    \where \protected {
      \func Relation1 : alp st1 bet = alp *> bet
        => rewrite (pmap (\lam z => alp *> z) (LeftHorizontalWhiskering-relation bet), idp_*>) idp

      \func Relation2  : alp st2 bet = bet *> alp
        => rewrite (pmap (\lam z => z *> alp) (LeftHorizontalWhiskering-relation bet), idp_*>)idp

      \func Relation3  : alp st1 bet = alp st2 bet => Relation alp bet
    }
}