Require Import Spaces.Nat.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export HoTT.Classes.interfaces.canonical_names.
Require Import Modalities.ReflectiveSubuniverse.

Local Set Polymorphic Inductive Cumulativity.

Generalizable Variables A B f g x y.

(* 
For various structures we omit declaration of substructures. For example, if we 
say:

Class Setoid_Morphism :=
  { setoidmor_a : Setoid A
  ; setoidmor_b : Setoid B
  ; sm_proper : Proper ((=) ==> (=)) f }.
#[export] Existing Instances setoidmor_a setoidmor_b sm_proper.

then each time a Setoid instance is required, Coq will try to prove that a
Setoid_Morphism exists. This obviously results in an enormous blow-up of the
search space. Moreover, one should be careful to declare a Setoid_Morphisms
as a substructure. Consider [f t1 t2], now if we want to perform setoid rewriting
in [t2] Coq will first attempt to prove that [f t1] is Proper, for which it will 
attempt to prove [Setoid_Morphism (f t1)]. If many structures declare
Setoid_Morphism as a substructure, setoid rewriting will become horribly slow.
*)

(* An unbundled variant of the former CoRN CSetoid. We do not 
  include a proof that A is a Setoid because it can be derived. *)
Class IsApart A {Aap : Apart A} : Type :=
  { apart_set : IsHSet A
  ; apart_mere : is_mere_relation _ apart
  ; apart_symmetric : Symmetric (≶)
  ; apart_cotrans : CoTransitive (≶)
  ; tight_apart : forall x y, ~(x ≶ y) <-> x = y }.
#[export] Existing Instances
  apart_set
  apart_mere
  apart_symmetric
  apart_cotrans.

Global Instance apart_irrefl `{IsApart A} : Irreflexive (≶).
A: Type
Aap: Apart A
H: IsApart A
Irreflexive apart
Proof.
A: Type
Aap: Apart A
H: IsApart A
Irreflexive apart
intros x ap.
A: Type
Aap: Apart A
H: IsApart A
x: A
ap: x ≶ x
Empty
apply (tight_apart x x).
A: Type
Aap: Apart A
H: IsApart A
x: A
ap: x ≶ x
x = x
A: Type
Aap: Apart A
H: IsApart A
x: A
ap: x ≶ x
x ≶ x
-
A: Type
Aap: Apart A
H: IsApart A
x: A
ap: x ≶ x
x = x reflexivity.
-
A: Type
Aap: Apart A
H: IsApart A
x: A
ap: x ≶ x
x ≶ x assumption.
Qed.

Arguments tight_apart {A Aap IsApart} _ _.

Section setoid_morphisms.
  Context {A B} {Aap : Apart A} {Bap : Apart B} (f : A -> B).

  Class StrongExtensionality := strong_extensionality : forall x y, f x ≶ f y -> x ≶ y.
End setoid_morphisms.

(* HOTT TODO check if this is ok/useful *)
#[export]
Hint Extern 4 (?f _ = ?f _) => eapply (ap f) : core.

Section setoid_binary_morphisms.
  Context {A B C} {Aap: Apart A} 
    {Bap : Apart B} {Cap : Apart C} (f : A -> B -> C).

  Class StrongBinaryExtensionality := strong_binary_extensionality
    : forall x₁ y₁ x₂ y₂, f x₁ y₁ ≶ f x₂ y₂ -> hor (x₁ ≶ x₂) (y₁ ≶ y₂).
End setoid_binary_morphisms.

(*
Since apartness usually only becomes relevant when considering fields (e.g. the 
real numbers), we do not include it in the lower part of the algebraic hierarchy
(as opposed to CoRN).
*)
Section upper_classes.
  Universe i.
  Context (A : Type@{i}).

  Local Open Scope mc_mult_scope.

  Class IsSemiGroup {Aop: SgOp A} :=
    { sg_set : IsHSet A
    ; sg_ass : Associative (.*.) }.
    #[export] Existing Instances sg_set sg_ass.

  Class IsCommutativeSemiGroup {Aop : SgOp A} :=
    { comsg_sg : @IsSemiGroup (.*.)
    ; comsg_comm : Commutative (.*.) }.
  #[export] Existing Instances comsg_sg comsg_comm.

  Class IsSemiLattice {Aop : SgOp A} :=
    { semilattice_sg : @IsCommutativeSemiGroup (.*.)
    ; semilattice_idempotent : BinaryIdempotent (.*.)}.
  #[export] Existing Instances semilattice_sg semilattice_idempotent.

  Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
    { monoid_semigroup : IsSemiGroup
    ; monoid_left_id : LeftIdentity (.*.) mon_unit
    ; monoid_right_id : RightIdentity (.*.) mon_unit }.
  #[export] Existing Instances
    monoid_semigroup
    monoid_left_id
    monoid_right_id.

  Class IsCommutativeMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
    { commonoid_mon : @IsMonoid (.*.) Aunit
    ; commonoid_commutative : Commutative (.*.) }.
  #[export] Existing Instances
    commonoid_mon
    commonoid_commutative.

  Class IsGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
    { group_monoid : @IsMonoid (.*.) Aunit
    ; negate_l : LeftInverse (.*.) (-) mon_unit
    ; negate_r : RightInverse (.*.) (-) mon_unit }.
  #[export] Existing Instances 
    group_monoid
    negate_l
    negate_r.

  Class IsBoundedSemiLattice {Aop : SgOp A} {Aunit : MonUnit A} :=
    { bounded_semilattice_mon : @IsCommutativeMonoid (.*.) Aunit
    ; bounded_semilattice_idempotent : BinaryIdempotent (.*.)}.
  #[export] Existing Instances
    bounded_semilattice_mon
    bounded_semilattice_idempotent.

  Class IsAbGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
    { abgroup_group : @IsGroup (.*.) Aunit Anegate
    ; abgroup_commutative : Commutative (.*.) }.
  #[export] Existing Instances abgroup_group abgroup_commutative.

  Close Scope mc_mult_scope.

  Context {Aplus : Plus A} {Amult : Mult A} {Azero : Zero A} {Aone : One A}.

  Class IsSemiCRing :=
    { semiplus_monoid : @IsCommutativeMonoid plus_is_sg_op zero_is_mon_unit
    ; semimult_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
    ; semiring_distr : LeftDistribute (.*.) (+)
    ; semiring_left_absorb : LeftAbsorb (.*.) 0 }.
  #[export] Existing Instances semiplus_monoid semimult_monoid semiring_distr semiring_left_absorb.

  Context {Anegate : Negate A}.

  Class IsRing := {
    ring_abgroup :: @IsAbGroup plus_is_sg_op zero_is_mon_unit _;
    ring_monoid :: @IsMonoid mult_is_sg_op one_is_mon_unit;
    ring_dist_left :: LeftDistribute (.*.) (+);
    ring_dist_right :: RightDistribute (.*.) (+);
  }.

  Class IsCRing :=
    { cring_group : @IsAbGroup plus_is_sg_op zero_is_mon_unit _
    ; cring_monoid : @IsCommutativeMonoid mult_is_sg_op one_is_mon_unit
    ; cring_dist : LeftDistribute (.*.) (+) }.

  #[export] Existing Instances cring_group cring_monoid cring_dist.

  Global Instance isring_iscring : IsCRing -> IsRing.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
IsCRing -> IsRing
  Proof.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
IsCRing -> IsRing
    intros H.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing
IsRing
    econstructor; try exact _.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing
RightDistribute mult plus
    intros a b c.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing
a, b, c: A
(a + b) * c = a * c + b * c
    lhs rapply commutativity.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing
a, b, c: A
sg_op c (a + b) = a * c + b * c
    lhs rapply distribute_l.
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing
a, b, c: A
c * a + c * b = a * c + b * c
    f_ap; apply commutativity.
  Defined.

  Class IsIntegralDomain :=
    { intdom_ring : IsCRing
    ; intdom_nontrivial : PropHolds (not (1 = 0))
    ; intdom_nozeroes : NoZeroDivisors A }.
  #[export] Existing Instances intdom_nozeroes.

  (* We do not include strong extensionality for (-) and (/)
    because it can de derived *)
  Class IsField {Aap: Apart A} {Arecip: Recip A} :=
    { field_ring : IsCRing
    ; field_apart : IsApart A
    ; field_plus_ext : StrongBinaryExtensionality (+)
    ; field_mult_ext : StrongBinaryExtensionality (.*.)
    ; field_nontrivial : PropHolds (1 ≶ 0)
    ; recip_inverse : forall x, x.1 // x = 1 }.
  #[export] Existing Instances
    field_ring
    field_apart
    field_plus_ext
    field_mult_ext.

  (* We let /0 = 0 so properties as Injective (/),
    f (/x) = / (f x), / /x = x, /x * /y = /(x * y) 
    hold without any additional assumptions *)
  Class IsDecField {Adec_recip : DecRecip A} :=
    { decfield_ring : IsCRing
    ; decfield_nontrivial : PropHolds (1 <> 0)
    ; dec_recip_0 : /0 = 0
    ; dec_recip_inverse : forall x, x <> 0 -> x / x = 1 }.
  #[export] Existing Instances decfield_ring.

  Class FieldCharacteristic@{j} {Aap : Apart@{i j} A} (k : nat) : Type@{j}
    := field_characteristic : forall n : nat,
        Nat.Core.lt 0 n ->
        iff@{j j j} (forall m : nat, not@{j} (paths@{Set} n
                                                  (Nat.Core.mul k m)))
        (@apart A Aap (nat_iter n (1 +) 0) 0).

End upper_classes.

(* Due to bug #2528 *)
#[export]
Hint Extern 4 (PropHolds (1 <> 0)) =>
  eapply @intdom_nontrivial : typeclass_instances.
#[export]
Hint Extern 5 (PropHolds (1 ≶ 0)) =>
  eapply @field_nontrivial : typeclass_instances.
#[export]
Hint Extern 5 (PropHolds (1 <> 0)) =>
  eapply @decfield_nontrivial : typeclass_instances.

(* 
For a strange reason IsCRing instances of Integers are sometimes obtained by
Integers -> IntegralDomain -> Ring and sometimes directly. Making this an
instance with a low priority instead of using intdom_ring:> IsCRing forces Coq to
take the right way 
*)
#[export]
Hint Extern 10 (IsCRing _) => apply @intdom_ring : typeclass_instances.

Arguments recip_inverse {A Aplus Amult Azero Aone Anegate Aap Arecip IsField} _.
Arguments dec_recip_inverse
  {A Aplus Amult Azero Aone Anegate Adec_recip IsDecField} _ _.
Arguments dec_recip_0 {A Aplus Amult Azero Aone Anegate Adec_recip IsDecField}.

Section lattice.
  Context A {Ajoin: Join A} {Ameet: Meet A} {Abottom : Bottom A} {Atop : Top A}.

  Class IsJoinSemiLattice := 
    join_semilattice : @IsSemiLattice A join_is_sg_op.
  #[export] Existing Instance join_semilattice.
  Class IsBoundedJoinSemiLattice := 
    bounded_join_semilattice : @IsBoundedSemiLattice A
      join_is_sg_op bottom_is_mon_unit.
  #[export] Existing Instance bounded_join_semilattice.
  Class IsMeetSemiLattice :=
    meet_semilattice : @IsSemiLattice A meet_is_sg_op.
  #[export] Existing Instance meet_semilattice.
  Class IsBoundedMeetSemiLattice :=
    bounded_meet_semilattice : @IsBoundedSemiLattice A
      meet_is_sg_op top_is_mon_unit.
  #[export] Existing Instance bounded_meet_semilattice.


  Class IsLattice := 
    { lattice_join : IsJoinSemiLattice
    ; lattice_meet : IsMeetSemiLattice
    ; join_meet_absorption : Absorption (⊔) (⊓) 
    ; meet_join_absorption : Absorption (⊓) (⊔) }.
  #[export] Existing Instances
    lattice_join
    lattice_meet
    join_meet_absorption 
    meet_join_absorption.

  Class IsBoundedLattice :=
    { boundedlattice_join : IsBoundedJoinSemiLattice
    ; boundedlattice_meet : IsBoundedMeetSemiLattice
    ; boundedjoin_meet_absorption : Absorption (⊔) (⊓)
    ; boundedmeet_join_absorption : Absorption (⊓) (⊔)}.
  #[export] Existing Instances
    boundedlattice_join
    boundedlattice_meet
    boundedjoin_meet_absorption
    boundedmeet_join_absorption.


  Class IsDistributiveLattice := 
    { distr_lattice_lattice : IsLattice
    ; join_meet_distr_l : LeftDistribute (⊔) (⊓) }.
  #[export] Existing Instances distr_lattice_lattice join_meet_distr_l.
End lattice.

Section morphism_classes.

  Section sgmorphism_classes.
  Context {A B : Type} {Aop : SgOp A} {Bop : SgOp B}
    {Aunit : MonUnit A} {Bunit : MonUnit B}.

  Local Open Scope mc_mult_scope.

  Class IsSemiGroupPreserving (f : A -> B) :=
    preserves_sg_op : forall x y, f (x * y) = f x * f y.

  Class IsUnitPreserving (f : A -> B) :=
    preserves_mon_unit : f mon_unit = mon_unit.

  Class IsMonoidPreserving (f : A -> B) :=
    { monmor_sgmor : IsSemiGroupPreserving f
    ; monmor_unitmor : IsUnitPreserving f }.
  #[export] Existing Instances monmor_sgmor monmor_unitmor.
  End sgmorphism_classes.

  Section ringmorphism_classes.
  Context {A B : Type} {Aplus : Plus A} {Bplus : Plus B}
    {Amult : Mult A} {Bmult : Mult B} {Azero : Zero A} {Bzero : Zero B}
    {Aone : One A} {Bone : One B}.

  Class IsSemiRingPreserving (f : A -> B) :=
    { semiringmor_plus_mor : @IsMonoidPreserving A B
        plus_is_sg_op plus_is_sg_op zero_is_mon_unit zero_is_mon_unit f
    ; semiringmor_mult_mor : @IsMonoidPreserving A B
        mult_is_sg_op mult_is_sg_op one_is_mon_unit one_is_mon_unit f }.
  #[export] Existing Instances semiringmor_plus_mor semiringmor_mult_mor.

  Context {Aap : Apart A} {Bap : Apart B}.
  Class IsSemiRingStrongPreserving (f : A -> B) :=
    { strong_semiringmor_sr_mor : IsSemiRingPreserving f
    ; strong_semiringmor_strong_mor : StrongExtensionality f }.
  #[export] Existing Instances strong_semiringmor_sr_mor strong_semiringmor_strong_mor.
  End ringmorphism_classes.

  Section latticemorphism_classes.
  Context {A B : Type} {Ajoin : Join A} {Bjoin : Join B}
    {Ameet : Meet A} {Bmeet : Meet B}.

  Class IsJoinPreserving (f : A -> B) :=
    join_slmor_sgmor : @IsSemiGroupPreserving A B join_is_sg_op join_is_sg_op f.
  #[export] Existing Instances join_slmor_sgmor.

  Class IsMeetPreserving (f : A -> B) :=
    meet_slmor_sgmor : @IsSemiGroupPreserving A B meet_is_sg_op meet_is_sg_op f.
  #[export] Existing Instances meet_slmor_sgmor.

  Context {Abottom : Bottom A} {Bbottom : Bottom B}.
  Class IsBoundedJoinPreserving (f : A -> B) := bounded_join_slmor_monmor
      : @IsMonoidPreserving A B join_is_sg_op join_is_sg_op
         bottom_is_mon_unit bottom_is_mon_unit f.
  #[export] Existing Instances bounded_join_slmor_monmor.

  Class IsLatticePreserving (f : A -> B) :=
    { latticemor_join_mor : IsJoinPreserving f
    ; latticemor_meet_mor : IsMeetPreserving f }.
  #[export] Existing Instances
    latticemor_join_mor
    latticemor_meet_mor.
  End latticemorphism_classes.
End morphism_classes.

Section jections.
  Context {A B} (f : A -> B).

  Class IsInjective := injective : forall x y, f x = f y -> x = y.

  Lemma isinjective_ne `{!IsInjective} x y :
    x <> y -> f x <> f y.
A, B: Type
f: A -> B
H: IsInjective
x, y: A
x <> y -> f x <> f y
  Proof.
A, B: Type
f: A -> B
H: IsInjective
x, y: A
x <> y -> f x <> f y
    intros E1 E2.
A, B: Type
f: A -> B
H: IsInjective
x, y: A
E1: x <> y
E2: f x = f y
Empty apply E1.
A, B: Type
f: A -> B
H: IsInjective
x, y: A
E1: x <> y
E2: f x = f y
x = y
    apply injective.
A, B: Type
f: A -> B
H: IsInjective
x, y: A
E1: x <> y
E2: f x = f y
f x = f y
    assumption.
  Qed.

End jections.

Global Instance isinj_idmap A : @IsInjective A A idmap
  := fun x y => idmap.

#[export]
Hint Unfold IsInjective : typeclass_instances.

#[export]
Instance isinjective_mapinO_tr {A B : Type} (f : A -> B)
  {p : MapIn (Tr (-1)) f} : IsInjective f
  := fun x y pfeq => ap pr1 (@center _ (p (f y) (x; pfeq) (y; idpath))).

Section strong_injective.
  Context {A B} {Aap : Apart A} {Bap : Apart B} (f : A -> B) .
  Class IsStrongInjective :=
    { strong_injective : forall x y, x ≶ y -> f x ≶ f y
    ; strong_injective_mor : StrongExtensionality f }.
End strong_injective.

Section extras.

Class CutMinusSpec A (cm : CutMinus A) `{Zero A} `{Plus A} `{Le A} := {
  cut_minus_le : forall x y, y ≤ x -> x ∸ y + y = x ;
  cut_minus_0 : forall x y, x ≤ y -> x ∸ y = 0
}.


Global Instance ishprop_issemigrouppreserving `{Funext} {A B : Type} `{IsHSet B}
  `{SgOp A} `{SgOp B} {f : A -> B} : IsHProp (IsSemiGroupPreserving f).
H: Funext
A, B: Type
IsHSet0: IsHSet B
H0: SgOp A
H1: SgOp B
f: A -> B
IsHProp (IsSemiGroupPreserving f)
Proof.
H: Funext
A, B: Type
IsHSet0: IsHSet B
H0: SgOp A
H1: SgOp B
f: A -> B
IsHProp (IsSemiGroupPreserving f)
  unfold IsSemiGroupPreserving; exact _.
Defined.

Definition issig_IsSemiRingPreserving {A B : Type}
  `{Plus A, Plus B, Mult A, Mult B, Zero A, Zero B, One A, One B} {f : A -> B}
  : _ <~> IsSemiRingPreserving f := ltac:(issig).

Definition issig_IsMonoidPreserving {A B : Type} `{SgOp A} `{SgOp B}
  `{MonUnit A} `{MonUnit B} {f : A -> B} : _ <~> IsMonoidPreserving f
  := ltac:(issig).

Global Instance ishprop_ismonoidpreserving `{Funext} {A B : Type} `{SgOp A}
  `{SgOp B} `{IsHSet B} `{MonUnit A} `{MonUnit B} (f : A -> B)
  : IsHProp (IsMonoidPreserving f).
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp (IsMonoidPreserving f)
Proof.
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp (IsMonoidPreserving f)
  srapply (istrunc_equiv_istrunc _ issig_IsMonoidPreserving).
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp
  {_ : IsSemiGroupPreserving f & IsUnitPreserving f}
  srapply (istrunc_equiv_istrunc _ (equiv_sigma_prod0 _ _)^-1).
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp (IsSemiGroupPreserving f * IsUnitPreserving f)
  srapply istrunc_prod.
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp (IsUnitPreserving f)
  unfold IsUnitPreserving.
H: Funext
A, B: Type
H0: SgOp A
H1: SgOp B
IsHSet0: IsHSet B
H2: MonUnit A
H3: MonUnit B
f: A -> B
IsHProp (f mon_unit = mon_unit)
  exact _.
Defined.

Global Instance ishprop_issemiringpreserving `{Funext} {A B : Type} `{IsHSet B}
  `{Plus A, Plus B, Mult A, Mult B, Zero A, Zero B, One A, One B}
  (f : A -> B)
  : IsHProp (IsSemiRingPreserving f).
H: Funext
A, B: Type
IsHSet0: IsHSet B
H0: Plus A
H1: Plus B
H2: Mult A
H3: Mult B
H4: Zero A
H5: Zero B
H6: One A
H7: One B
f: A -> B
IsHProp (IsSemiRingPreserving f)
Proof.
H: Funext
A, B: Type
IsHSet0: IsHSet B
H0: Plus A
H1: Plus B
H2: Mult A
H3: Mult B
H4: Zero A
H5: Zero B
H6: One A
H7: One B
f: A -> B
IsHProp (IsSemiRingPreserving f)
  snrapply (istrunc_equiv_istrunc _ issig_IsSemiRingPreserving).
H: Funext
A, B: Type
IsHSet0: IsHSet B
H0: Plus A
H1: Plus B
H2: Mult A
H3: Mult B
H4: Zero A
H5: Zero B
H6: One A
H7: One B
f: A -> B
IsHProp
  {_ : IsMonoidPreserving f & IsMonoidPreserving f}
  exact _.
Defined.

Definition issig_issemigroup x y : _ <~> @IsSemiGroup x y := ltac:(issig).

Global Instance ishprop_issemigroup `{Funext}
  : forall x y, IsHProp (@IsSemiGroup x y).
H: Funext
forall (x : Type) (y : SgOp x),
IsHProp (IsSemiGroup x)
Proof.
H: Funext
forall (x : Type) (y : SgOp x),
IsHProp (IsSemiGroup x)
  intros x y; apply istrunc_S; intros a b.
H: Funext
x: Type
y: SgOp x
a, b: IsSemiGroup x
Contr (a = b)
  rewrite <- (eisretr (issig_issemigroup x y) a).
H: Funext
x: Type
y: SgOp x
a, b: IsSemiGroup x
Contr
  (issig_issemigroup x y
     ((issig_issemigroup x y)^-1 a) = b)
  rewrite <- (eisretr (issig_issemigroup x y) b).
H: Funext
x: Type
y: SgOp x
a, b: IsSemiGroup x
Contr
  (issig_issemigroup x y
     ((issig_issemigroup x y)^-1 a) =
   issig_issemigroup x y
     ((issig_issemigroup x y)^-1 b))
  set (a' := (issig_issemigroup x y)^-1 a).
H: Funext
x: Type
y: SgOp x
a, b: IsSemiGroup x
a':= (issig_issemigroup x y)^-1 a: {_ : IsHSet x & Associative sg_op}
Contr
  (issig_issemigroup x y a' =
   issig_issemigroup x y
     ((issig_issemigroup x y)^-1 b))
  set (b' := (issig_issemigroup x y)^-1 b).
H: Funext
x: Type
y: SgOp x
a, b: IsSemiGroup x
a':= (issig_issemigroup x y)^-1 a: {_ : IsHSet x & Associative sg_op}
b':= (issig_issemigroup x y)^-1 b: {_ : IsHSet x & Associative sg_op}
Contr
  (issig_issemigroup x y a' = issig_issemigroup x y b')
  clearbody a' b'; clear a b.
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
Contr
  (issig_issemigroup x y a' = issig_issemigroup x y b')
  srapply (contr_equiv _ (ap (issig_issemigroup x y))).
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
Contr (a' = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) a').
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
Contr
  ((equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     (equiv_sigma_prod0 (IsHSet x) (Associative sg_op)
        a') = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) b').
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
Contr
  ((equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     (equiv_sigma_prod0 (IsHSet x) (Associative sg_op)
        a') =
   (equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     (equiv_sigma_prod0 (IsHSet x) (Associative sg_op)
        b'))
  set (a := equiv_sigma_prod0 _ _ a').
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
a:= equiv_sigma_prod0 (IsHSet x) (Associative sg_op) a': (IsHSet x * Associative sg_op)%type
Contr
  ((equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     a =
   (equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     (equiv_sigma_prod0 (IsHSet x) (Associative sg_op)
        b'))
  set (b := equiv_sigma_prod0 _ _ b').
H: Funext
x: Type
y: SgOp x
a', b': {_ : IsHSet x & Associative sg_op}
a:= equiv_sigma_prod0 (IsHSet x) (Associative sg_op) a': (IsHSet x * Associative sg_op)%type
b:= equiv_sigma_prod0 (IsHSet x) (Associative sg_op) b': (IsHSet x * Associative sg_op)%type
Contr
  ((equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     a =
   (equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     b)
  clearbody a b; clear a' b'.
H: Funext
x: Type
y: SgOp x
a, b: (IsHSet x * Associative sg_op)%type
Contr
  ((equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     a =
   (equiv_sigma_prod0 (IsHSet x) (Associative sg_op))^-1
     b)
  srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)).
H: Funext
x: Type
y: SgOp x
a, b: (IsHSet x * Associative sg_op)%type
Contr (a = b)
  srapply (contr_equiv _ (equiv_path_prod _ _)).
H: Funext
x: Type
y: SgOp x
a, b: (IsHSet x * Associative sg_op)%type
Contr ((fst a = fst b) * (snd a = snd b))
  srapply contr_prod.
H: Funext
x: Type
y: SgOp x
a, b: (IsHSet x * Associative sg_op)%type
Contr (snd a = snd b)
  destruct a as [a' a], b as [b' b].
H: Funext
x: Type
y: SgOp x
a': IsHSet x
a: Associative sg_op
b': IsHSet x
b: Associative sg_op
Contr (snd (a', a) = snd (b', b))
  do 3 (nrefine (contr_equiv' _ (@equiv_path_forall H _ _ _ _));
  nrefine (@contr_forall H _ _ _); intro).
H: Funext
x: Type
y: SgOp x
a': IsHSet x
a: Associative sg_op
b': IsHSet x
b: Associative sg_op
a0, a1, a2: x
Contr (snd (a', a) a0 a1 a2 = snd (b', b) a0 a1 a2)
  exact _.
Defined.

Definition issig_ismonoid x y z : _ <~> @IsMonoid x y z := ltac:(issig).

Global Instance ishprop_ismonoid `{Funext} x y z : IsHProp (@IsMonoid x y z).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
IsHProp (IsMonoid x)
Proof.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
IsHProp (IsMonoid x)
  apply istrunc_S.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
forall x0 y0 : IsMonoid x, Contr (x0 = y0)
  intros a b.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: IsMonoid x
Contr (a = b)
  rewrite <- (eisretr (issig_ismonoid x y z) a).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: IsMonoid x
Contr
  (issig_ismonoid x y z ((issig_ismonoid x y z)^-1 a) =
   b)
  rewrite <- (eisretr (issig_ismonoid x y z) b).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: IsMonoid x
Contr
  (issig_ismonoid x y z ((issig_ismonoid x y z)^-1 a) =
   issig_ismonoid x y z ((issig_ismonoid x y z)^-1 b))
  set (a' := (issig_ismonoid x y z)^-1 a).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: IsMonoid x
a':= (issig_ismonoid x y z)^-1 a: {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr
  (issig_ismonoid x y z a' =
   issig_ismonoid x y z ((issig_ismonoid x y z)^-1 b))
  set (b' := (issig_ismonoid x y z)^-1 b).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: IsMonoid x
a':= (issig_ismonoid x y z)^-1 a: {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
b':= (issig_ismonoid x y z)^-1 b: {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr
  (issig_ismonoid x y z a' = issig_ismonoid x y z b')
  clearbody a' b'; clear a b.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr
  (issig_ismonoid x y z a' = issig_ismonoid x y z b')
  srapply (contr_equiv _ (ap (issig_ismonoid x y z))).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr (a' = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) a').
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr
  ((equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1
     (equiv_sigma_prod0 (IsSemiGroup x)
        {_ : LeftIdentity sg_op mon_unit &
        RightIdentity sg_op mon_unit} a') = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) b').
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
Contr
  ((equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1
     (equiv_sigma_prod0 (IsSemiGroup x)
        {_ : LeftIdentity sg_op mon_unit &
        RightIdentity sg_op mon_unit} a') =
   (equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1
     (equiv_sigma_prod0 (IsSemiGroup x)
        {_ : LeftIdentity sg_op mon_unit &
        RightIdentity sg_op mon_unit} b'))
  set (a := equiv_sigma_prod0 _ _ a').
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
a:= equiv_sigma_prod0 (IsSemiGroup x)
  {_ : LeftIdentity sg_op mon_unit &
  RightIdentity sg_op mon_unit} a': (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1
     (equiv_sigma_prod0 (IsSemiGroup x)
        {_ : LeftIdentity sg_op mon_unit &
        RightIdentity sg_op mon_unit} b'))
  set (b := equiv_sigma_prod0 _ _ b').
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': {_ : IsSemiGroup x &
{_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}}
a:= equiv_sigma_prod0 (IsSemiGroup x)
  {_ : LeftIdentity sg_op mon_unit &
  RightIdentity sg_op mon_unit} a': (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
b:= equiv_sigma_prod0 (IsSemiGroup x)
  {_ : LeftIdentity sg_op mon_unit &
  RightIdentity sg_op mon_unit} b': (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1 b)
  clearbody a b; clear a' b'.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsSemiGroup x)
      {_ : LeftIdentity sg_op mon_unit &
      RightIdentity sg_op mon_unit})^-1 b)
  srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr (a = b)
  srapply (contr_equiv _ (equiv_path_prod _ _)).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr ((fst a = fst b) * (snd a = snd b))
  srapply contr_prod.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a, b: (IsSemiGroup x *
 {_ : LeftIdentity sg_op mon_unit &
 RightIdentity sg_op mon_unit})%type
Contr (snd a = snd b)
  destruct a as [a' a], b as [b' b]; cbn.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a': IsSemiGroup x
a: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
b': IsSemiGroup x
b: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
Contr (a = b)
  rewrite <- (eissect (equiv_sigma_prod0 _ _) a).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a': IsSemiGroup x
a: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
b': IsSemiGroup x
b: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
Contr
  ((equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1
     (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
        (RightIdentity sg_op mon_unit) a) = b)
  rewrite <- (eissect (equiv_sigma_prod0 _ _) b).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a': IsSemiGroup x
a: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
b': IsSemiGroup x
b: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
Contr
  ((equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1
     (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
        (RightIdentity sg_op mon_unit) a) =
   (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1
     (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
        (RightIdentity sg_op mon_unit) b))
  set (a'' := equiv_sigma_prod0 _ _ a).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a': IsSemiGroup x
a: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
b': IsSemiGroup x
b: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
a'':= equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
  (RightIdentity sg_op mon_unit) a: (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
Contr
  ((equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1 a'' =
   (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1
     (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
        (RightIdentity sg_op mon_unit) b))
  set (b'' := equiv_sigma_prod0 _ _ b).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a': IsSemiGroup x
a: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
b': IsSemiGroup x
b: {_ : LeftIdentity sg_op mon_unit &
RightIdentity sg_op mon_unit}
a'':= equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
  (RightIdentity sg_op mon_unit) a: (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
b'':= equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
  (RightIdentity sg_op mon_unit) b: (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
Contr
  ((equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1 a'' =
   (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1 b'')
  clearbody a'' b''; clear a b.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a'', b'': (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
Contr
  ((equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1 a'' =
   (equiv_sigma_prod0 (LeftIdentity sg_op mon_unit)
      (RightIdentity sg_op mon_unit))^-1 b'')
  srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a'', b'': (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
Contr (a'' = b'')
  srapply (contr_equiv _ (equiv_path_prod _ _)).
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a'', b'': (LeftIdentity sg_op mon_unit * RightIdentity sg_op mon_unit)%type
Contr ((fst a'' = fst b'') * (snd a'' = snd b''))
  destruct a'' as [a a''], b'' as [b b'']; cbn.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
Contr ((a = b) * (a'' = b''))
  snrapply contr_prod.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
Contr (a = b)
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
Contr (a'' = b'')
  all: srapply contr_paths_contr.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
Contr (LeftIdentity sg_op mon_unit)
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
Contr (RightIdentity sg_op mon_unit)
  all: srapply contr_inhabited_hprop.
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
IsHProp (LeftIdentity sg_op mon_unit)
H: Funext
x: Type
y: SgOp x
z: MonUnit x
a', b': IsSemiGroup x
a: LeftIdentity sg_op mon_unit
a'': RightIdentity sg_op mon_unit
b: LeftIdentity sg_op mon_unit
b'': RightIdentity sg_op mon_unit
IsHProp (RightIdentity sg_op mon_unit)
  all: srapply istrunc_forall.
Defined.

Definition issig_isgroup w x y z : _ <~> @IsGroup w x y z := ltac:(issig).

Global Instance ishprop_isgroup `{Funext} w x y z : IsHProp (@IsGroup w x y z).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
IsHProp (IsGroup w)
Proof.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
IsHProp (IsGroup w)
  apply istrunc_S.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
forall x0 y0 : IsGroup w, Contr (x0 = y0)
  intros a b.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: IsGroup w
Contr (a = b)
  rewrite <- (eisretr (issig_isgroup w x y z) a).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: IsGroup w
Contr
  (issig_isgroup w x y z
     ((issig_isgroup w x y z)^-1 a) = b)
  rewrite <- (eisretr (issig_isgroup w x y z) b).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: IsGroup w
Contr
  (issig_isgroup w x y z
     ((issig_isgroup w x y z)^-1 a) =
   issig_isgroup w x y z
     ((issig_isgroup w x y z)^-1 b))
  set (a' := (issig_isgroup w x y z)^-1 a).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: IsGroup w
a':= (issig_isgroup w x y z)^-1 a: {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr
  (issig_isgroup w x y z a' =
   issig_isgroup w x y z
     ((issig_isgroup w x y z)^-1 b))
  set (b' := (issig_isgroup w x y z)^-1 b).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: IsGroup w
a':= (issig_isgroup w x y z)^-1 a: {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
b':= (issig_isgroup w x y z)^-1 b: {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr
  (issig_isgroup w x y z a' = issig_isgroup w x y z b')
  clearbody a' b'; clear a b.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr
  (issig_isgroup w x y z a' = issig_isgroup w x y z b')
  srapply (contr_equiv _ (ap (issig_isgroup w x y z))).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr (a' = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) a').
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr
  ((equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1
     (equiv_sigma_prod0 (IsMonoid w)
        {_ : LeftInverse sg_op negate mon_unit &
        RightInverse sg_op negate mon_unit} a') = b')
  rewrite <- (eissect (equiv_sigma_prod0 _ _) b').
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
Contr
  ((equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1
     (equiv_sigma_prod0 (IsMonoid w)
        {_ : LeftInverse sg_op negate mon_unit &
        RightInverse sg_op negate mon_unit} a') =
   (equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1
     (equiv_sigma_prod0 (IsMonoid w)
        {_ : LeftInverse sg_op negate mon_unit &
        RightInverse sg_op negate mon_unit} b'))
  set (a := equiv_sigma_prod0 _ _ a').
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
a:= equiv_sigma_prod0 (IsMonoid w)
  {_ : LeftInverse sg_op negate mon_unit &
  RightInverse sg_op negate mon_unit} a': (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1
     (equiv_sigma_prod0 (IsMonoid w)
        {_ : LeftInverse sg_op negate mon_unit &
        RightInverse sg_op negate mon_unit} b'))
  set (b := equiv_sigma_prod0 _ _ b').
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': {_ : IsMonoid w &
{_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}}
a:= equiv_sigma_prod0 (IsMonoid w)
  {_ : LeftInverse sg_op negate mon_unit &
  RightInverse sg_op negate mon_unit} a': (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
b:= equiv_sigma_prod0 (IsMonoid w)
  {_ : LeftInverse sg_op negate mon_unit &
  RightInverse sg_op negate mon_unit} b': (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1 b)
  clearbody a b; clear a' b'.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr
  ((equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1 a =
   (equiv_sigma_prod0 (IsMonoid w)
      {_ : LeftInverse sg_op negate mon_unit &
      RightInverse sg_op negate mon_unit})^-1 b)
  srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr (a = b)
  srapply (contr_equiv _ (equiv_path_prod _ _)).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr ((fst a = fst b) * (snd a = snd b))
  srapply contr_prod.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a, b: (IsMonoid w *
 {_ : LeftInverse sg_op negate mon_unit &
 RightInverse sg_op negate mon_unit})%type
Contr (snd a = snd b)
  destruct a as [a' a], b as [b' b]; cbn.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a': IsMonoid w
a: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
b': IsMonoid w
b: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
Contr (a = b)
  rewrite <- (eissect (equiv_sigma_prod0 _ _) a).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a': IsMonoid w
a: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
b': IsMonoid w
b: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
Contr
  ((equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1
     (equiv_sigma_prod0
        (LeftInverse sg_op negate mon_unit)
        (RightInverse sg_op negate mon_unit) a) = b)
  rewrite <- (eissect (equiv_sigma_prod0 _ _) b).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a': IsMonoid w
a: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
b': IsMonoid w
b: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
Contr
  ((equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1
     (equiv_sigma_prod0
        (LeftInverse sg_op negate mon_unit)
        (RightInverse sg_op negate mon_unit) a) =
   (equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1
     (equiv_sigma_prod0
        (LeftInverse sg_op negate mon_unit)
        (RightInverse sg_op negate mon_unit) b))
  set (a'' := equiv_sigma_prod0 _ _ a).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a': IsMonoid w
a: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
b': IsMonoid w
b: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
a'':= equiv_sigma_prod0
  (LeftInverse sg_op negate mon_unit)
  (RightInverse sg_op negate mon_unit) a: (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
Contr
  ((equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1 a'' =
   (equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1
     (equiv_sigma_prod0
        (LeftInverse sg_op negate mon_unit)
        (RightInverse sg_op negate mon_unit) b))
  set (b'' := equiv_sigma_prod0 _ _ b).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a': IsMonoid w
a: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
b': IsMonoid w
b: {_ : LeftInverse sg_op negate mon_unit &
RightInverse sg_op negate mon_unit}
a'':= equiv_sigma_prod0
  (LeftInverse sg_op negate mon_unit)
  (RightInverse sg_op negate mon_unit) a: (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
b'':= equiv_sigma_prod0
  (LeftInverse sg_op negate mon_unit)
  (RightInverse sg_op negate mon_unit) b: (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
Contr
  ((equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1 a'' =
   (equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1 b'')
  clearbody a'' b''; clear a b.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a'', b'': (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
Contr
  ((equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1 a'' =
   (equiv_sigma_prod0
      (LeftInverse sg_op negate mon_unit)
      (RightInverse sg_op negate mon_unit))^-1 b'')
  srapply (contr_equiv _ (ap (equiv_sigma_prod0 _ _)^-1)).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a'', b'': (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
Contr (a'' = b'')
  srapply (contr_equiv _ (equiv_path_prod _ _)).
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a'', b'': (LeftInverse sg_op negate mon_unit * RightInverse sg_op negate mon_unit)%type
Contr ((fst a'' = fst b'') * (snd a'' = snd b''))
  destruct a'' as [a a''], b'' as [b b'']; cbn.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
Contr ((a = b) * (a'' = b''))
  srapply contr_prod.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
Contr (a = b)
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
Contr (a'' = b'')
  all: srapply contr_paths_contr.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
Contr (LeftInverse sg_op negate mon_unit)
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
Contr (RightInverse sg_op negate mon_unit)
  all: srapply contr_inhabited_hprop.
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
IsHProp (LeftInverse sg_op negate mon_unit)
H: Funext
w: Type
x: SgOp w
y: MonUnit w
z: Negate w
a', b': IsMonoid w
a: LeftInverse sg_op negate mon_unit
a'': RightInverse sg_op negate mon_unit
b: LeftInverse sg_op negate mon_unit
b'': RightInverse sg_op negate mon_unit
IsHProp (RightInverse sg_op negate mon_unit)
  all: srapply istrunc_forall.
Defined.

End extras.