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

Local Set Polymorphic Inductive Cumulativity.

Generalizable Variables A B C 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 }.

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 (.*.) }.

  Class IsCommutativeSemiGroup {Aop : SgOp A} :=
    { comsg_sg :: @IsSemiGroup (.*.)
    ; comsg_comm :: Commutative (.*.) }.

  Class IsSemiLattice {Aop : SgOp A} :=
    { semilattice_sg :: @IsCommutativeSemiGroup (.*.)
    ; semilattice_idempotent :: BinaryIdempotent (.*.)}.

  Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
    { monoid_semigroup :: IsSemiGroup
    ; monoid_left_id :: LeftIdentity (.*.) mon_unit
    ; monoid_right_id :: RightIdentity (.*.) mon_unit }.

  Class IsCommutativeMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
    { commonoid_mon :: @IsMonoid (.*.) Aunit
    ; commonoid_commutative :: Commutative (.*.) }.

  Class IsGroup {Aop : SgOp A} {Aunit : MonUnit A} {Ainv : Inverse A} :=
    { group_monoid :: @IsMonoid (.*.) mon_unit
    ; inverse_l :: LeftInverse (.*.) (^) mon_unit
    ; inverse_r :: RightInverse (.*.) (^) mon_unit
    }.

  Class IsBoundedSemiLattice {Aop : SgOp A} {Aunit : MonUnit A} :=
    { bounded_semilattice_mon :: @IsCommutativeMonoid (.*.) Aunit
    ; bounded_semilattice_idempotent :: BinaryIdempotent (.*.)}.

  Local Close Scope mc_mult_scope.

  Class IsAbGroup {Aop : SgOp A} {Aunit : MonUnit A} {Ainv : Inverse A} :=
    { abgroup_group :: @IsGroup Aop Aunit Ainv
    ; abgroup_commutative :: Commutative Aop }.

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

  Class IsSemiCRing :=
    { semiplus_monoid :: @IsCommutativeMonoid (+) 0
    ; semimult_monoid :: @IsCommutativeMonoid (.*.) 1
    ; semiring_distr :: LeftDistribute (.*.) (+)
    ; semiring_left_absorb :: LeftAbsorb (.*.) 0 }.

  Context {Anegate : Negate A}.

  Class IsRing :=
    { ring_abgroup :: @IsAbGroup (+) 0 (-)
    ; ring_monoid :: @IsMonoid (.*.) 1
    ; ring_dist_left :: LeftDistribute (.*.) (+)
    ; ring_dist_right :: RightDistribute (.*.) (+)
  }.

  Class IsCRing :=
    { cring_group :: @IsAbGroup (+) 0 (-)
    ; cring_monoid :: @IsCommutativeMonoid (.*.) 1
    ; cring_dist :: LeftDistribute (.*.) (+) }.

  #[export] 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 }.

  (* We do not include strong extensionality for (-) and (/)
    because it can be 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 }.

  (* 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 }.

  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_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.

  Class IsBoundedJoinSemiLattice :=
    bounded_join_semilattice :: @IsBoundedSemiLattice A
      join_is_sg_op bottom_is_mon_unit.

  Class IsMeetSemiLattice :=
    meet_semilattice :: @IsSemiLattice A meet_is_sg_op.

  Class IsBoundedMeetSemiLattice :=
    bounded_meet_semilattice :: @IsBoundedSemiLattice A
      meet_is_sg_op top_is_mon_unit.

  Class IsLattice :=
    { lattice_join :: IsJoinSemiLattice
    ; lattice_meet :: IsMeetSemiLattice
    ; join_meet_absorption :: Absorption (⊔) (⊓)
    ; meet_join_absorption :: Absorption (⊓) (⊔) }.

  Class IsBoundedLattice :=
    { boundedlattice_join :: IsBoundedJoinSemiLattice
    ; boundedlattice_meet :: IsBoundedMeetSemiLattice
    ; boundedjoin_meet_absorption :: Absorption (⊔) (⊓)
    ; boundedmeet_join_absorption :: Absorption (⊓) (⊔)}.

  Class IsDistributiveLattice :=
    { distr_lattice_lattice :: IsLattice
    ; join_meet_distr_l :: LeftDistribute (⊔) (⊓) }.

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 }.

  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
        (+) (+) 0 0 f
    ; semiringmor_mult_mor :: @IsMonoidPreserving A B
        (.*.) (.*.) 1 1 f }.

  Context {Aap : Apart A} {Bap : Apart B}.
  Class IsSemiRingStrongPreserving (f : A -> B) :=
    { strong_semiringmor_sr_mor :: IsSemiRingPreserving f
    ; strong_semiringmor_strong_mor :: StrongExtensionality f }.

  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.

  Class IsMeetPreserving (f : A -> B) :=
    meet_slmor_sgmor :: @IsSemiGroupPreserving A B meet_is_sg_op meet_is_sg_op f.

  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.

  Class IsLatticePreserving (f : A -> B) :=
    { latticemor_join_mor :: IsJoinPreserving f
    ; latticemor_meet_mor :: IsMeetPreserving f }.

  End latticemorphism_classes.
End morphism_classes.

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

  #[export] 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.

  #[export] 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) (sg_op x y) = sg_op ((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 (sg_op x y)) = sg_op (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 (sg_op 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 = sg_op (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 (sg_op 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 (sg_op (f x) (f y)) = sg_op (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) exact _.
    -
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;[|exact (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 (sg_op x y) = sg_op (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 (sg_op x y)) = f (sg_op (f^-1 x) (f^-1 y))
    lhs napply 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
sg_op x y = f (sg_op (f^-1 x) (f^-1 y))
    symmetry.
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 (sg_op (f^-1 x) (f^-1 y)) = sg_op x y
    lhs napply fp.
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
sg_op (f (f^-1 x)) (f (f^-1 y)) = sg_op x y
    f_ap; 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 exact _.
    -
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; exact 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.

#[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
}.

#[export] Instance istrunc_isunitpreserving `{Funext} {n A B} unitA unitB f
  : IsTrunc n.+1 B -> IsTrunc n (@IsUnitPreserving A B unitA unitB f).
H: Funext
n: trunc_index
A, B: Type
unitA: MonUnit A
unitB: MonUnit B
f: A -> B
IsTrunc n.+1 B -> IsTrunc n (IsUnitPreserving f)
Proof.
H: Funext
n: trunc_index
A, B: Type
unitA: MonUnit A
unitB: MonUnit B
f: A -> B
IsTrunc n.+1 B -> IsTrunc n (IsUnitPreserving f)
  unfold IsUnitPreserving; exact _.
Defined.

#[export] Instance istrunc_issemigrouppreserving `{Funext} {n A B} opA opB f
  : IsTrunc n.+1 B -> IsTrunc n (@IsSemiGroupPreserving A B opA opB f).
H: Funext
n: trunc_index
A, B: Type
opA: SgOp A
opB: SgOp B
f: A -> B
IsTrunc n.+1 B -> IsTrunc n (IsSemiGroupPreserving f)
Proof.
H: Funext
n: trunc_index
A, B: Type
opA: SgOp A
opB: SgOp B
f: A -> B
IsTrunc n.+1 B -> IsTrunc n (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).

#[export] Instance ishprop_ismonoidpreserving `{Funext} {A B : Type} `{SgOp A}
  `{SgOp B} `{IsHSet B} `{MonUnit A} `{MonUnit B} (f : A -> B)
  : IsHProp (IsMonoidPreserving f)
  := istrunc_equiv_istrunc _ issig_IsMonoidPreserving.

#[export] 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)
  := istrunc_equiv_istrunc _ issig_IsSemiRingPreserving.

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

#[export] Instance ishprop_issemigroup `{Funext} x y
  : IsHProp (@IsSemiGroup x y)
  := istrunc_equiv_istrunc _ (issig_issemigroup _ _).

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

#[export] Instance ishprop_ismonoid `{Funext} x y z : IsHProp (@IsMonoid x y z)
  := istrunc_equiv_istrunc _ (issig_ismonoid _ _ _).

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

#[export] Instance ishprop_isgroup `{Funext} w x y z : IsHProp (@IsGroup w x y z)
  := istrunc_equiv_istrunc _ (issig_isgroup _ _ _ _).

End extras.