@include logic.pg

section Magma

variable (G : ★);
def binop := G → G → G;

def = := eq G;
infixl 1 =;

variable (* : binop);
infixl 20 *;

def *> (a b : G) := b * a;
infixl 20 *>;

section Semigroup

def assoc := forall (a b c : G), a * (b * c) = a * b * c;
hypothesis (Hassoc : assoc);

def assoc_op (a b c : G) : a *> (b *> c) = a *> b *> c := 
    eq_sym G (a *> b *> c) (a *> (b *> c)) (Hassoc c b a);

section Monoid

variable (e : G);
def id_l := forall (a : G), e * a = a;
def id_r := forall (a : G), a * e = a;

hypothesis (Hid_l : id_l);
hypothesis (Hid_r : id_r);

def id_l_op : forall (a : G), e *> a = a := Hid_r;
def id_r_op : forall (a : G), a *> e = a := Hid_l;

def left_id_unique (a : G) : #id_l G (*) a → a = e :=
    fun (H : #id_l G (*) a) =>
        eq_trans G a (a * e) e
            (eq_sym G (a * e) a (Hid_r a))
            (H e);

def right_id_unique (a : G) : #id_r G (*) a → a = e := #left_id_unique G (*>) e Hid_l a;

section Group

variable (i : G → G);
hypothesis (Hinv_l : forall (a : G), i a * a = e);
hypothesis (Hinv_r : forall (a : G), a * i a = e);

def left_inv_unique (a b : G) (h : b * a = e) : b = i a :=
    eq_trans G b (b * e) (i a)
        (eq_sym G (b * e) b (Hid_r b))
        (eq_trans G (b * e) (b * (a * i a)) (i a)
            (eq_cong G G e (a * i a) ((*) b)
                (eq_sym G (a * i a) e (Hinv_r a)))
            (eq_trans G (b * (a * i a)) (b * a * i a) (i a)
                (Hassoc b a (i a))
                (eq_trans G (b * a * i a) (e * i a) (i a)
                    (eq_cong G G (b * a) e ([z : G] z * i a) h)
                    (Hid_l (i a)))));

def right_inv_unique (a b : G) (h : a * b = e) : b = i a :=
    #left_inv_unique G (*>) assoc_op e Hid_r Hid_l i Hinv_l a b h;

def inverse_involutive (a : G) : i (i a) = a :=
    eq_sym G a (i (i a)) (right_inv_unique (i a) a (Hinv_l a));

def shoes_and_socks (a b : G) : i (a * b) = i b * i a :=
    eq_sym G (i b * i a) (i (a * b))
    (right_inv_unique (a * b) (i b * i a)
    (let
        (under_ai (x y : G) (h : x = y) := eq_cong G G x y ([z : G] z * (i a)) h)
     in
        eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
        (Hassoc (a * b) (i b) (i a))
        (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
            (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (Hassoc a b (i b))))
            (eq_trans G (a * (b * i b) * i a) (a * e * i a) e
                (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (Hinv_r b))
                (eq_trans G (a * e * i a) (a * i a) e
                    (under_ai (a * e) a (Hid_r a))
                    (Hinv_r a))))
     end));

def cancel_l (a b c : G) (h : a * b = a * c) : b = c :=
    eq_trans G b (e * b) c
        (eq_sym G (e * b) b (Hid_l b))
        (eq_trans G (e * b) (i a * a * b) c
            (eq_cong G G e (i a * a) ([x : G] x * b)
                (eq_sym G (i a * a) e (Hinv_l a)))
            (eq_trans G (i a * a * b) (i a * (a * b)) c
                (eq_sym G (i a * (a * b)) (i a * a * b) (Hassoc (i a) a b))
                (eq_trans G (i a * (a * b)) (i a * (a * c)) c
                    (eq_cong G G (a * b) (a * c) ((*) (i a)) h)
                    (eq_trans G (i a * (a * c)) (i a * a * c) c
                        (Hassoc (i a) a c)
                        (eq_trans G (i a * a * c) (e * c) c
                            (eq_cong G G (i a * a) e ([x : G] x * c) (Hinv_l a))
                            (Hid_l c))))));

def cancel_r (a b c : G) (h : b * a = c * a) : b = c :=
    #cancel_l G (*>) assoc_op e Hid_r i Hinv_r a b c h;

def abelian : ★ := forall (a b : G), a * b = b * a;

def left_right_cancel : (forall (x y z : G), x * y = z * x → y = z) → abelian :=
    fun (h : forall (x y z : G), x * y = z * x → y = z) (a b : G) =>
        h (i a) (a * b) (b * a)
        (eq_trans G (i a * (a * b)) (i a * a * b) (b * a * i a)
            (Hassoc (i a) a b)
            (eq_trans G (i a * a * b) (e * b) (b * a * i a)
                (eq_cong G G (i a * a) e ([x : G] x * b) (Hinv_l a))
                (eq_trans G (e * b) b (b * a * i a)
                    (Hid_l b)
                    (eq_trans G b (b * e) (b * a * i a)
                        (eq_sym G (b * e) b (Hid_r b))
                        (eq_trans G (b * e) (b * (a * i a)) (b * a * i a)
                            (eq_cong G G e (a * i a) ((*) b) (eq_sym G (a * i a) e (Hinv_r a)))
                            (Hassoc b a (i a)))))));

def inv_distrib_abelian : (forall (a b : G), i (a * b) = i a * i b) → abelian :=
    fun (h : forall (a b : G), i (a * b) = i a * i b) (a b : G) =>
        eq_trans G (a * b) (i (i a) * b) (b * a)
            (eq_cong G G a (i (i a)) ([x : G] x * b) (eq_sym G (i (i a)) a (inverse_involutive a)))
            (eq_trans G (i (i a) * b) (i (i a) * i (i b)) (b * a)
                (eq_cong G G b (i (i b)) ((*) (i (i a))) (eq_sym G (i (i b)) b (inverse_involutive b)))
                (eq_trans G (i (i a) * i (i b)) (i (i b * i a)) (b * a)
                    (eq_sym G (i (i b * i a)) (i (i a) * i (i b)) (shoes_and_socks (i b) (i a)))
                    (eq_trans G (i (i b * i a)) (i (i b) * i (i a)) (b * a)
                        (h (i b) (i a))
                        (eq_trans G (i (i b) * i (i a)) (b * i (i a)) (b * a)
                            (eq_cong G G (i (i b)) b ([x : G] x * i (i a)) (inverse_involutive b))
                            (eq_cong G G (i (i a)) a ((*) b) (inverse_involutive a))))));

def order_two (a : G) : a * a = e → a = i a := right_inv_unique a a;

def all_order_two_abelian : (forall (a : G), a * a = e) → abelian :=
    fun (h : forall (a : G), a * a = e) =>
        inv_distrib_abelian (fun (a b : G) =>
            (eq_trans G (i (a * b)) (a * b) (i a * i b)
                (eq_sym G (a * b) (i (a * b)) (order_two (a * b) (h (a * b))))
                (eq_trans G (a * b) (a * i b) (i a * i b)
                    (eq_cong G G b (i b) ((*) a) (order_two b (h b)))
                    (eq_cong G G a (i a) ([x : G] x * i b) (order_two a (h a))))));

end Group
end Monoid
end Semigroup
end Magma