Require Import
  HoTT.Classes.interfaces.abstract_algebra.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope mc_mult_scope.
Generalizable Variables G H A B C f g.

Section group_props.
  Context `{IsGroup G}.

  (** Group inverses are involutive *)
  #[export] Instance inverse_involutive : Involutive (^).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
Involutive inv
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
Involutive inv
    intros x.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = x
    transitivity (mon_unit * x).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = 1 * x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
1 * x = x
    2: apply left_identity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = 1 * x
    transitivity ((x^^ *  x^) * x).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * x^ * x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ * x^ * x = 1 * x
    2: apply (@ap _ _ (fun y => y * x)),
          left_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * x^ * x
    transitivity (x^^ * (x^ * x)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * (x^ * x)
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ * (x^ * x) = (x^)^ * x^ * x
    2: apply associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * (x^ * x)
    transitivity (x^^ * mon_unit).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * 1
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ * 1 = (x^)^ * (x^ * x)
    2: apply ap, symmetry, left_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x: G
(x^)^ = (x^)^ * 1
    apply symmetry, right_identity.
  Qed.

  #[export] Instance isinj_group_inverse : IsInjective (^).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
IsInjective inv
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
IsInjective inv
    intros x y E.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
E: x^ = y^
x = y
    refine ((involutive x)^ @ _ @ involutive y).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
E: x^ = y^
(x^)^ = (y^)^
    apply ap, E.
  Qed.

  Lemma inverse_mon_unit : mon_unit^ = mon_unit.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
1^ = 1
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
1^ = 1
    change ((fun x => mon_unit^ = x) mon_unit).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
(fun x : G => 1^ = x) 1
    apply (transport _ (left_inverse mon_unit)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
1^ = 1^ * 1
    apply symmetry, right_identity.
  Qed.

  #[export] Instance group_cancelL : forall z : G, LeftCancellation (.*.) z.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
forall z : G, LeftCancellation sg_op z
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
forall z : G, LeftCancellation sg_op z
    intros z x y E.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = y
    rhs_V rapply left_identity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = 1 * y
    rhs_V exact (ap (.* y) (left_inverse z)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = z^ * z * y
    rhs_V rapply simple_associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = z^ * (z * y)
    rhs_V rapply (ap (-z *.) E).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = - z * (z * x)
    symmetry.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
- z * (z * x) = x
    lhs rapply simple_associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
- z * z * x = x
    lhs exact (ap (.* x) (left_inverse z)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: z * x = z * y
1 * x = x
    apply left_identity.
  Defined.

  #[export] Instance group_cancelR: forall z : G, RightCancellation (.*.) z.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
forall z : G, RightCancellation sg_op z
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
forall z : G, RightCancellation sg_op z
    intros z x y E.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
x = y
    rewrite <-(right_identity x).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
x * 1 = y
    rewrite <-(right_inverse (unit:=mon_unit) z).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
x * (z * z^) = y
    rewrite associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
x * z * z^ = y
    rewrite E.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
y * z * z^ = y
    rewrite <-(associativity y ), right_inverse, right_identity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
z, x, y: G
E: x * z = y * z
y = y
    reflexivity.
  Qed.

  Lemma inverse_sg_op x y : (x * y)^ = y^ * x^.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = y^ * x^
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = y^ * x^
    rewrite <- (left_identity (-y * -x)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = 1 * (- y * - x)
    rewrite <- (left_inverse (unit:=mon_unit) (x * y)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * y) * (- y * - x)
    rewrite <- simple_associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * y * (- y * - x))
    rewrite <- simple_associativity.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * (y * (- y * - x)))
    rewrite (associativity y).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * (y * - y * - x))
    rewrite right_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * (1 * - x))
    rewrite (left_identity (-x)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * (x * - x)
    rewrite right_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsGroup G
x, y: G
(x * y)^ = (x * y)^ * 1
    apply symmetry, right_identity.
  Qed.

End group_props.

Section abgroup_props.
  Local Open Scope mc_add_scope.

  Lemma negate_sg_op_distr `{IsAbGroup G} x y : -(x + y) = -x + -y.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
(x * y)^ = x^ - y
  Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
(x * y)^ = x^ - y
    path_via (-y + -x).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
(x * y)^ = y^ - x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
y^ - x = x^ - y
    -
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
(x * y)^ = y^ - x rapply inverse_sg_op.
    -
G: Type
Aop: SgOp G
Aunit: MonUnit G
Ainv: Inverse G
H: IsAbGroup G
x, y: G
y^ - x = x^ - y apply commutativity.
  Qed.

  Local Close Scope mc_add_scope.
End abgroup_props.

Section groupmor_props.

  Context `{IsGroup A} `{IsGroup B} {f : A -> B} `{!IsMonoidPreserving f}.

  Lemma preserves_inverse x : f x^ = (f x)^.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Ainv0: Inverse B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f x^ = (f x)^
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Ainv0: Inverse B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f x^ = (f x)^
    apply (left_cancellation (.*.) (f x)).
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Ainv0: Inverse B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f x * f x^ = f x * (f x)^
    rewrite <-preserves_sg_op.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Ainv0: Inverse B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f (x * x^) = f x * (f x)^
    rewrite 2!right_inverse.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Ainv0: Inverse B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f 1 = 1
    exact preserves_mon_unit.
  Qed.

End groupmor_props.

Section from_another_sg.

  Context
    `{IsSemiGroup A} `{IsHSet B}
    `{Bop : SgOp B} (f : B -> A) `{!IsInjective f}
    (op_correct : forall x y, f (x * y) = f x * f y).

  Lemma projected_sg: IsSemiGroup B.
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsSemiGroup B
  Proof.
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsSemiGroup B
  split.
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsHSet B
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Associative sg_op
  -
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsHSet B exact _.
  -
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Associative sg_op repeat intro; apply (injective f).
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
x, y, z: B
f (x * (y * z)) = f (x * y * z)
    rewrite !op_correct.
A: Type
Aop: SgOp A
H: IsSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
x, y, z: B
f x * (f y * f z) = f x * f y * f z apply associativity.
  Qed.
End from_another_sg.

Section from_another_com.

  Context `{SgOp A} `{!Commutative (A:=A) sg_op} {B}
   `{Bop : SgOp B} (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x * y) = f x * f y).

  Lemma projected_comm : Commutative (A:=B) sg_op.
A: Type
H: SgOp A
Commutative0: Commutative sg_op
B: Type
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Commutative sg_op
  Proof.
A: Type
H: SgOp A
Commutative0: Commutative sg_op
B: Type
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Commutative sg_op
    intros x y.
A: Type
H: SgOp A
Commutative0: Commutative sg_op
B: Type
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
x, y: B
x * y = y * x
    apply (injective f).
A: Type
H: SgOp A
Commutative0: Commutative sg_op
B: Type
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
x, y: B
f (x * y) = f (y * x)
    rewrite 2!op_correct.
A: Type
H: SgOp A
Commutative0: Commutative sg_op
B: Type
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
x, y: B
f x * f y = f y * f x
    apply commutativity.
  Qed.

End from_another_com.

Section from_another_com_sg.

  Context
    `{IsCommutativeSemiGroup A} `{IsHSet B}
    `{Bop : SgOp B} (f : B -> A) `{!IsInjective f}
    (op_correct : forall x y, f (x * y) = f x * f y).

  Lemma projected_com_sg : IsCommutativeSemiGroup B.
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsCommutativeSemiGroup B
  Proof.
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsCommutativeSemiGroup B
    split.
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsSemiGroup B
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Commutative sg_op
    -
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
IsSemiGroup B apply (projected_sg f);assumption.
    -
A: Type
Aop: SgOp A
H: IsCommutativeSemiGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
Commutative sg_op apply (projected_comm f);assumption.
  Qed.

End from_another_com_sg.

Section from_another_monoid.

  Context `{IsMonoid A} `{IsHSet B}
   `{Bop : SgOp B} `{Bunit : MonUnit B} (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x * y) = f x * f y) (unit_correct : f mon_unit = mon_unit).

  Lemma projected_monoid : IsMonoid B.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsMonoid B
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsMonoid B
    split.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsSemiGroup B
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
LeftIdentity sg_op 1
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
RightIdentity sg_op 1
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsSemiGroup B apply (projected_sg f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
forall x y : B, f (x * y) = f x * f y assumption.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
LeftIdentity sg_op 1 repeat intro; apply (injective f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
y: B
f (1 * y) = f y
      rewrite op_correct, unit_correct, left_identity.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
y: B
f y = f y
      reflexivity.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
RightIdentity sg_op 1 repeat intro; apply (injective f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
x: B
f (x * 1) = f x
      rewrite op_correct, unit_correct, right_identity.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
x: B
f x = f x
      reflexivity.
  Qed.

End from_another_monoid.

Section from_another_com_monoid.

  Context
   `{IsCommutativeMonoid A} `{IsHSet B}
   `{Bop : SgOp B} `{Bunit : MonUnit B} (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x * y) = f x * f y)
   (unit_correct : f mon_unit = mon_unit).

  Lemma projected_com_monoid : IsCommutativeMonoid B.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsCommutativeMonoid B
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsCommutativeMonoid B
    split.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsMonoid B
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
Commutative sg_op
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
IsMonoid B apply (projected_monoid f);assumption.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsCommutativeMonoid A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
Commutative sg_op apply (projected_comm f);assumption.
  Qed.

End from_another_com_monoid.

Section from_another_group.

  Context
    `{isg : IsGroup A} `{IsHSet B}
    `{Bop : SgOp B} `{Bunit : MonUnit B} `{Binv : Inverse B}
    (f : B -> A) `{!IsInjective f}
    (op_correct : forall x y, f (x * y) = f x * f y)
    (unit_correct : f mon_unit = mon_unit)
    (inverse_correct : forall x, f x^ = (f x)^).

  Lemma projected_group : IsGroup B.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
IsGroup B
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
IsGroup B
    split.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
IsMonoid B
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
LeftInverse sg_op inv 1
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
RightInverse sg_op inv 1
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
IsMonoid B apply (projected_monoid f);assumption.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
LeftInverse sg_op inv 1 repeat intro; apply (injective f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
x: B
f (x^ * x) = f 1
      rewrite op_correct, inverse_correct, unit_correct, left_inverse.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
x: B
1 = 1
      apply reflexivity.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
RightInverse sg_op inv 1 repeat intro; apply (injective f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
x: B
f (x * x^) = f 1
      rewrite op_correct, inverse_correct, unit_correct, right_inverse.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
isg: IsGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Binv: Inverse B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
inverse_correct: forall x : B, f x^ = (f x)^
x: B
1 = 1
      reflexivity.
  Qed.

End from_another_group.

Section from_another_ab_group.
  Local Open Scope mc_add_scope.

  Context `{IsAbGroup A} `{IsHSet B}
   `{Bop : SgOp B} `{Bunit : MonUnit B} `{Bnegate : Negate B}
   (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x + y) = f x + f y)
   (unit_correct : f 0 = 0)
   (negate_correct : forall x, f (-x) = -f x).

  Lemma projected_ab_group : IsAbGroup B.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
IsAbGroup B
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
IsAbGroup B
    split.
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
IsGroup B
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
Commutative Bop
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
IsGroup B apply (projected_group f (isg:=abgroup_group _)); assumption.
    -
A: Type
Aop: SgOp A
Aunit: MonUnit A
Ainv: Inverse A
H: IsAbGroup A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x * y) = f x * f y
unit_correct: f 1 = 1
negate_correct: forall x : B, f x^ = (f x)^
Commutative Bop apply (projected_comm f); assumption.
  Qed.

  Local Close Scope mc_add_scope.
End from_another_ab_group.