groups.v

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 *)
  Global Instance negate_involutive : Involutive (-).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
Involutive negate
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
Involutive negate
    intros x.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = x
    transitivity (mon_unit * x).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = mon_unit * x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
mon_unit * x = x
    2: apply left_identity.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = mon_unit * x
    transitivity ((- - x * - x) * x).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * - x * x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x * - x * x = mon_unit * x
    2: apply (@ap _ _ (fun y => y * x)),
          left_inverse.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * - x * x
    transitivity (- - x * (- x * x)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * (- x * x)
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x * (- x * x) = - - x * - x * x
    2: apply associativity.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * (- x * x)
    transitivity (- - x * mon_unit).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * mon_unit
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x * mon_unit = - - x * (- x * x)
    2: apply ap, symmetry, left_inverse.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
- - x = - - x * mon_unit
    apply symmetry, right_identity.
  Qed.

  Global Instance isinj_group_negate : IsInjective (-).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
IsInjective negate
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
IsInjective negate
    intros x y E.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
x, y: G
E: - x = - y
- - x = - - y
    apply ap, E.
  Qed.

  Lemma negate_mon_unit : - mon_unit = mon_unit.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
- mon_unit = mon_unit
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
- mon_unit = mon_unit
    change ((fun x => - mon_unit = x) mon_unit).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
(fun x : G => - mon_unit = x) mon_unit
    apply (transport _ (left_inverse mon_unit)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
- mon_unit = - mon_unit * mon_unit
    apply symmetry, right_identity.
  Qed.

  Global Instance group_cancelL : forall z : G, LeftCancellation (.*.) z.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall z : G, LeftCancellation sg_op z
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall z : G, LeftCancellation sg_op z
    intros z x y E.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
z, x, y: G
E: z * x = z * y
x = mon_unit * y
    rhs_V rapply (ap (.* y) (left_inverse z)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
z, x, y: G
E: z * x = z * y
- z * z * x = x
    lhs rapply (ap (.* x) (left_inverse z)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
z, x, y: G
E: z * x = z * y
mon_unit * x = x
    apply left_identity.
  Defined.

  Global Instance group_cancelR: forall z : G, RightCancellation (.*.) z.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall z : G, RightCancellation sg_op z
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall z : G, RightCancellation sg_op z
    intros z x y E.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
z, x, y: G
E: x * z = y * z
x * mon_unit = y
    rewrite <-(right_inverse (unit:=mon_unit) z).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
z, x, y: G
E: x * z = y * z
y = y
    reflexivity.
  Qed.

  Lemma negate_sg_op x y : - (x * y) = -y * -x.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = - y * - x
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = - y * - x
    rewrite <- (left_identity (-y * -x)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = mon_unit * (- y * - x)
    rewrite <- (left_inverse (unit:=mon_unit) (x * y)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate 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
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = - (x * y) * (x * (mon_unit * - x))
    rewrite (left_identity (-x)).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = - (x * y) * (x * - x)
    rewrite right_inverse.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
- (x * y) = - (x * y) * mon_unit
    apply symmetry, right_identity.
  Qed.

End group_props.

Section abgroup_props.

  Lemma negate_sg_op_distr `{IsAbGroup G} x y : -(x * y) = -x * -y.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- (x * y) = - x * - y
  Proof.G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- (x * y) = - x * - y
    path_via (-y * -x).G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- (x * y) = - y * - x
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- y * - x = - x * - y
    -G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- (x * y) = - y * - x apply negate_sg_op.
    -G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsAbGroup G
x, y: G
- y * - x = - x * - y apply commutativity.
  Qed.

End abgroup_props.

Section groupmor_props.

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

  Lemma preserves_negate x : f (-x) = -f x.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Anegate0: Negate 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
Anegate: Negate A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Anegate0: Negate 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
Anegate: Negate A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Anegate0: Negate 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
Anegate: Negate A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Anegate0: Negate 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
Anegate: Negate A
H: IsGroup A
B: Type
Aop0: SgOp B
Aunit0: MonUnit B
Anegate0: Negate B
H0: IsGroup B
f: A -> B
IsMonoidPreserving0: IsMonoidPreserving f
x: A
f mon_unit = mon_unit
    apply 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 apply _.
  -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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
LeftIdentity sg_op mon_unit
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 mon_unit = mon_unit
RightIdentity sg_op mon_unit
    -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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
LeftIdentity sg_op mon_unit 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 mon_unit = mon_unit
y: B
f (mon_unit * 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 mon_unit = mon_unit
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 mon_unit = mon_unit
RightIdentity sg_op mon_unit 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 mon_unit = mon_unit
x: B
f (x * mon_unit) = 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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
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 mon_unit = mon_unit
Commutative sg_op apply (projected_comm f);assumption.
  Qed.

End from_another_com_monoid.

Section from_another_group.

  Context
    `{IsGroup 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 mon_unit = mon_unit)
    (negate_correct : forall x, f (-x) = -f x).

  Lemma projected_group : IsGroup B.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsGroup B
  Proof.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsGroup B
    split.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsMonoid B
A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
LeftInverse sg_op negate mon_unit
A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
RightInverse sg_op negate mon_unit
    -A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsMonoid B apply (projected_monoid f);assumption.
    -A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
LeftInverse sg_op negate mon_unit repeat intro; apply (injective f).A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
x: B
f (- x * x) = f mon_unit
      rewrite op_correct, negate_correct, unit_correct, left_inverse.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
x: B
mon_unit = mon_unit
      apply reflexivity.
    -A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
RightInverse sg_op negate mon_unit repeat intro; apply (injective f).A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
x: B
f (x * - x) = f mon_unit
      rewrite op_correct, negate_correct, unit_correct, right_inverse.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate A
H: IsGroup 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
x: B
mon_unit = mon_unit
      reflexivity.
  Qed.

End from_another_group.

Section from_another_ab_group.

  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 mon_unit = mon_unit)
   (negate_correct : forall x, f (-x) = -f x).

  Lemma projected_ab_group : IsAbGroup B.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsAbGroup B
  Proof.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsAbGroup B
    split.A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsGroup B
A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
Commutative sg_op
    -A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
IsGroup B apply (projected_group f);assumption.
    -A: Type
Aop: SgOp A
Aunit: MonUnit A
Anegate: Negate 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 mon_unit = mon_unit
negate_correct: forall x : B, f (- x) = - f x
Commutative sg_op apply (projected_comm f);assumption.
  Qed.

End from_another_ab_group.

Section id_mor.

  Context `{SgOp A} `{MonUnit A}.

  Global Instance id_sg_morphism : IsSemiGroupPreserving (@id A).A: Type
H: SgOp A
H0: MonUnit A
IsSemiGroupPreserving id
  Proof.A: Type
H: SgOp A
H0: MonUnit A
IsSemiGroupPreserving id
    split.
  Defined.

  Global Instance id_monoid_morphism : IsMonoidPreserving (@id A).A: Type
H: SgOp A
H0: MonUnit A
IsMonoidPreserving id
  Proof.A: Type
H: SgOp A
H0: MonUnit A
IsMonoidPreserving id
    split; split.
  Defined.

End id_mor.

Section compose_mor.

  Context
    `{SgOp A} `{MonUnit A}
    `{SgOp B} `{MonUnit B}
    `{SgOp C} `{MonUnit C}
    (f : A -> B) (g : B -> C).

  (** Making these global instances causes typeclass loops.  Instead they are declared below as [Hint Extern]s that apply only when the goal has the specified form. *)
  Local Instance compose_sg_morphism : IsSemiGroupPreserving f -> IsSemiGroupPreserving g ->
    IsSemiGroupPreserving (g ∘ f).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
IsSemiGroupPreserving f ->
IsSemiGroupPreserving g ->
IsSemiGroupPreserving (g ∘ f)
  Proof.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
IsSemiGroupPreserving f ->
IsSemiGroupPreserving g ->
IsSemiGroupPreserving (g ∘ f)
    red; intros fp gp x y.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
(g ∘ f) (x * y) = (g ∘ f) x * (g ∘ f) y
    unfold Compose.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
g (f (x * y)) = g (f x) * g (f y)
    refine ((ap g _) @ _).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
f (x * y) = ?Goal
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
g ?Goal = g (f x) * g (f y)
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
f (x * y) = ?Goal apply fp.
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
fp: IsSemiGroupPreserving f
gp: IsSemiGroupPreserving g
x, y: A
g (f x * f y) = g (f x) * g (f y) apply gp.
  Defined.

  Local Instance compose_monoid_morphism : IsMonoidPreserving f -> IsMonoidPreserving g ->
    IsMonoidPreserving (g ∘ f).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
IsMonoidPreserving f ->
IsMonoidPreserving g -> IsMonoidPreserving (g ∘ f)
  Proof.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
IsMonoidPreserving f ->
IsMonoidPreserving g -> IsMonoidPreserving (g ∘ f)
    intros;split.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
IsSemiGroupPreserving (g ∘ f)
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
IsUnitPreserving (g ∘ f)
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
IsSemiGroupPreserving (g ∘ f) apply _.
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
IsUnitPreserving (g ∘ f) red;unfold Compose.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
g (f mon_unit) = mon_unit
      etransitivity;[|apply (preserves_mon_unit (f:=g))].A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
C: Type
H3: SgOp C
H4: MonUnit C
f: A -> B
g: B -> C
X: IsMonoidPreserving f
X0: IsMonoidPreserving g
g (f mon_unit) = g mon_unit
      apply ap,preserves_mon_unit.
  Defined.

End compose_mor.

Section invert_mor.

  Context
    `{SgOp A} `{MonUnit A}
    `{SgOp B} `{MonUnit B}
    (f : A -> B).

  Local Instance invert_sg_morphism
    : forall `{!IsEquiv f}, IsSemiGroupPreserving f ->
      IsSemiGroupPreserving (f^-1).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
forall IsEquiv0 : IsEquiv f,
IsSemiGroupPreserving f -> IsSemiGroupPreserving f^-1
  Proof.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
forall IsEquiv0 : IsEquiv f,
IsSemiGroupPreserving f -> IsSemiGroupPreserving f^-1
    red; intros E fp x y.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
f^-1 (x * y) = f^-1 x * f^-1 y
    apply (equiv_inj f).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
f (f^-1 (x * y)) = f (f^-1 x * f^-1 y)
    refine (_ @ _ @ _ @ _)^.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
f (f^-1 x * f^-1 y) = ?Goal1
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
?Goal1 = ?Goal0
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
?Goal0 = ?Goal
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
?Goal = f (f^-1 (x * y))
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
f (f^-1 x * f^-1 y) = ?Goal1 apply fp.
    (* We could use [apply ap2; apply eisretr] here, but it is convenient
       to have things in terms of ap. *)
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
f (f^-1 x) * f (f^-1 y) = ?Goal0 refine (ap (fun z => z * _) _); apply eisretr.
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
x * f (f^-1 y) = ?Goal refine (ap (fun z => _ * z) _); apply eisretr.
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
E: IsEquiv f
fp: IsSemiGroupPreserving f
x, y: B
x * y = f (f^-1 (x * y)) symmetry; apply eisretr.
  Defined.

  Local Instance invert_monoid_morphism :
    forall `{!IsEquiv f}, IsMonoidPreserving f -> IsMonoidPreserving (f^-1).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
forall IsEquiv0 : IsEquiv f,
IsMonoidPreserving f -> IsMonoidPreserving f^-1
  Proof.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
forall IsEquiv0 : IsEquiv f,
IsMonoidPreserving f -> IsMonoidPreserving f^-1
    intros;split.A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
IsSemiGroupPreserving f^-1
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
IsUnitPreserving f^-1
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
IsSemiGroupPreserving f^-1 apply _.
    -A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
IsUnitPreserving f^-1 apply (equiv_inj f).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
f (f^-1 mon_unit) = f mon_unit
      refine (_ @ _).A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
f (f^-1 mon_unit) = ?Goal
A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
?Goal = f mon_unit
      +A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
f (f^-1 mon_unit) = ?Goal apply eisretr.
      +A: Type
H: SgOp A
H0: MonUnit A
B: Type
H1: SgOp B
H2: MonUnit B
f: A -> B
IsEquiv0: IsEquiv f
X: IsMonoidPreserving f
mon_unit = f mon_unit symmetry; apply preserves_mon_unit.
  Defined.

End invert_mor.

#[export]
Hint Extern 4 (IsSemiGroupPreserving (_ ∘ _)) =>
  class_apply @compose_sg_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsMonoidPreserving (_ ∘ _)) =>
  class_apply @compose_monoid_morphism : typeclass_instances.

#[export]
Hint Extern 4 (IsSemiGroupPreserving (_ o _)) =>
  class_apply @compose_sg_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsMonoidPreserving (_ o _)) =>
  class_apply @compose_monoid_morphism : typeclass_instances.

#[export]
Hint Extern 4 (IsSemiGroupPreserving (_^-1)) =>
  class_apply @invert_sg_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsMonoidPreserving (_^-1)) =>
  class_apply @invert_monoid_morphism : typeclass_instances.