Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Trunc.Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Trunc.
Require Import Types.Sigma Types.Forall Types.Prod.
Require Import WildCat.Core WildCat.Induced WildCat.Equiv WildCat.Universe
  WildCat.Products.
Require Import (notations) Classes.interfaces.canonical_names.
Require Export (hints) Classes.interfaces.abstract_algebra.
Require Export (hints) Classes.interfaces.canonical_names.
Require Export Classes.interfaces.canonical_names (SgOp, sg_op,
    MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity,
    Associative, simple_associativity, associativity,
    LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity).
Export canonical_names.BinOpNotations.
Require Export Classes.interfaces.abstract_algebra (IsSemiGroup(..), sg_set, sg_ass,
    IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup,
    IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor,
    IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit).

Local Set Polymorphic Inductive Cumulativity.
Local Set Universe Minimization ToSet.

Local Open Scope mc_mult_scope.

(** * Monoids *)

(** ** Definition *)

Record Monoid := {
  monoid_type :> Type;
  monoid_sgop :: SgOp monoid_type;
  monoid_unit :: MonUnit monoid_type;
  monoid_ismonoid :: IsMonoid monoid_type;
}.

Arguments monoid_sgop {_}.
Arguments monoid_unit {_}.
Arguments monoid_ismonoid {_}.
Global Opaque monoid_ismonoid.

Definition issig_monoid : _ <~> Monoid := ltac:(issig).

Section MonoidLaws.
  Context {M : Monoid} (x y z : M).  
  Definition mnd_assoc := associativity x y z.
  Definition mnd_unit_l := left_identity x.
  Definition mnd_unit_r := right_identity x.
End MonoidLaws.

(** ** Monoid homomorphisms *)

Record MonoidHomomorphism (M N : Monoid) := {
  mnd_homo_map :> monoid_type M -> monoid_type N;
  ismonoidpreserving_mnd_homo :: IsMonoidPreserving mnd_homo_map;
}.

Arguments mnd_homo_map {M N}.
Arguments Build_MonoidHomomorphism {M N} _ _.
Arguments ismonoidpreserving_mnd_homo {M N} f : rename.

Definition issig_MonoidHomomorphism (M N : Monoid)
  : _ <~> MonoidHomomorphism M N
  := ltac:(issig).

(** ** Basics properties of monoid homomorphisms *)

Definition mnd_homo_op {M N : Monoid} (f : MonoidHomomorphism M N)
  : forall (x y : M), f (x * y) = f x * f y
  := monmor_sgmor. 

Definition mnd_homo_unit {M N : Monoid} (f : MonoidHomomorphism M N)
  : f mon_unit = mon_unit
  := monmor_unitmor.

Definition equiv_path_monoidhomomorphism `{Funext} {M N : Monoid}
  {f g : MonoidHomomorphism M N}
  : f == g <~> f = g.
H: Funext
M, N: Monoid
f, g: MonoidHomomorphism M N
f == g <~> f = g
Proof.
H: Funext
M, N: Monoid
f, g: MonoidHomomorphism M N
f == g <~> f = g
  refine ((equiv_ap (issig_MonoidHomomorphism M N)^-1 _ _)^-1 oE _).
H: Funext
M, N: Monoid
f, g: MonoidHomomorphism M N
f == g <~>
(issig_MonoidHomomorphism M N)^-1 f = (issig_MonoidHomomorphism M N)^-1 g
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Funext
M, N: Monoid
f, g: MonoidHomomorphism M N
f == g <~>
((issig_MonoidHomomorphism M N)^-1 f).1 =
((issig_MonoidHomomorphism M N)^-1 g).1
  apply equiv_path_forall.
Defined.

Instance ishset_monoidhomomorphism `{Funext} {M N : Monoid}
  : IsHSet (MonoidHomomorphism M N).
H: Funext
M, N: Monoid
IsHSet (MonoidHomomorphism M N)
Proof.
H: Funext
M, N: Monoid
IsHSet (MonoidHomomorphism M N)
  apply istrunc_S.
H: Funext
M, N: Monoid
is_mere_relation (MonoidHomomorphism M N) paths
  intros f g; apply (istrunc_equiv_istrunc _ equiv_path_monoidhomomorphism).
Defined.

Definition mnd_homo_id {M : Monoid} : MonoidHomomorphism M M
  := Build_MonoidHomomorphism idmap _.

Definition mnd_homo_compose {M N P : Monoid}
  : MonoidHomomorphism N P -> MonoidHomomorphism M N
  -> MonoidHomomorphism M P
  := fun f g => Build_MonoidHomomorphism (f o g) _.

(** ** Monoid Isomorphisms *)

Record MonoidIsomorphism (M N : Monoid) := {
  mnd_iso_homo :> MonoidHomomorphism M N;
  isequiv_mnd_iso :: IsEquiv mnd_iso_homo;
}.

Definition Build_MonoidIsomorphism' {M N : Monoid}
  (f : M <~> N) (h : IsMonoidPreserving f)
  : MonoidHomomorphism M N.
M, N: Monoid
f: M <~> N
h: IsMonoidPreserving f
MonoidHomomorphism M N
Proof.
M, N: Monoid
f: M <~> N
h: IsMonoidPreserving f
MonoidHomomorphism M N
  snapply Build_MonoidIsomorphism.
M, N: Monoid
f: M <~> N
h: IsMonoidPreserving f
MonoidHomomorphism M N
M, N: Monoid
f: M <~> N
h: IsMonoidPreserving f
IsEquiv ?mnd_iso_homo
  1: srapply Build_MonoidHomomorphism.
M, N: Monoid
f: M <~> N
h: IsMonoidPreserving f
IsEquiv {| mnd_homo_map := f; ismonoidpreserving_mnd_homo := h |}
  exact _.
Defined.

Definition issig_MonoidIsomorphism (M N : Monoid)
  : _ <~> MonoidIsomorphism M N
  := ltac:(issig).

Coercion equiv_mnd_iso {M N : Monoid}
  : MonoidIsomorphism M N -> M <~> N
  := fun f => Build_Equiv M N f _. 

Definition mnd_iso_id {M : Monoid} : MonoidIsomorphism M M
  := Build_MonoidIsomorphism _ _ mnd_homo_id _.

Definition mnd_iso_compose {M N P : Monoid}
  : MonoidIsomorphism N P -> MonoidIsomorphism M N
  -> MonoidIsomorphism M P
  := fun g f => Build_MonoidIsomorphism _ _ (mnd_homo_compose g f) _.

Definition mnd_iso_inverse {M N : Monoid}
  : MonoidIsomorphism M N -> MonoidIsomorphism N M
  := fun f => Build_MonoidIsomorphism _ _ (Build_MonoidHomomorphism f^-1 _) _.

Instance reflexive_monoidisomorphism
  : Reflexive MonoidIsomorphism
  := fun M => mnd_iso_id.

Instance symmetric_monoidisomorphism
  : Symmetric MonoidIsomorphism
  := fun M N => mnd_iso_inverse.

Instance transitive_monoidisomorphism
  : Transitive MonoidIsomorphism
  := fun M N P f g => mnd_iso_compose g f.

(** ** The category of monoids *)

Instance isgraph_monoid : IsGraph Monoid
  := Build_IsGraph Monoid MonoidHomomorphism.

Instance is01cat_monoid : Is01Cat Monoid
  := Build_Is01Cat Monoid _ (@mnd_homo_id) (@mnd_homo_compose).

Local Notation mnd_homo_map' M N
  := (@mnd_homo_map M N : _ -> (monoid_type M $-> _)).

Instance is2graph_monoid : Is2Graph Monoid
  := fun M N => isgraph_induced (mnd_homo_map' M N).

Instance isgraph_monoidhomomorphism {M N : Monoid} : IsGraph (M $-> N)
  := isgraph_induced (mnd_homo_map' M N).

Instance is01cat_monoidhomomorphism {M N : Monoid} : Is01Cat (M $-> N)
  := is01cat_induced (mnd_homo_map' M N).

Instance is0gpd_monoidhomomorphism {M N : Monoid} : Is0Gpd (M $-> N)
  := is0gpd_induced (mnd_homo_map' M N).

Instance is0functor_postcomp_monoidhomomorphism
  {M N P : Monoid} (h : N $-> P)
  : Is0Functor (@cat_postcomp Monoid _ _ M N P h).
M, N, P: Monoid
h: N $-> P
Is0Functor (cat_postcomp M h)
Proof.
M, N, P: Monoid
h: N $-> P
Is0Functor (cat_postcomp M h)
  apply Build_Is0Functor.
M, N, P: Monoid
h: N $-> P
forall a b : M $-> N, (a $-> b) -> cat_postcomp M h a $-> cat_postcomp M h b
  intros ? ? p a; exact (ap h (p a)).
Defined.

Instance is0functor_precomp_monoidhomomorphism
  {M N P : Monoid} (h : M $-> N)
  : Is0Functor (@cat_precomp Monoid _ _ M N P h).
M, N, P: Monoid
h: M $-> N
Is0Functor (cat_precomp P h)
Proof.
M, N, P: Monoid
h: M $-> N
Is0Functor (cat_precomp P h)
  apply Build_Is0Functor.
M, N, P: Monoid
h: M $-> N
forall a b : N $-> P, (a $-> b) -> cat_precomp P h a $-> cat_precomp P h b
  intros ? ? p; exact (p o h).
Defined.

Instance is1cat_monoid : Is1Cat Monoid.
Is1Cat Monoid
Proof.
Is1Cat Monoid
  by rapply Build_Is1Cat.
Defined.

Instance hasequivs_monoid : HasEquivs Monoid.
HasEquivs Monoid
Proof.
HasEquivs Monoid
  snapply Build_HasEquivs.
Monoid -> Monoid -> Type
forall a b : Monoid, (a $-> b) -> Type
forall a b : Monoid, ?CatEquiv' a b -> a $-> b
forall (a b : Monoid) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
forall (a b : Monoid) (f : a $-> b), ?CatIsEquiv' a b f -> ?CatEquiv' a b
forall (a b : Monoid) (f : a $-> b) (fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
forall a b : Monoid, ?CatEquiv' a b -> b $-> a
forall (a b : Monoid) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
forall (a b : Monoid) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
forall (a b : Monoid) (f : a $-> b) (g : b $-> a),
f $o g $== Id b -> g $o f $== Id a -> ?CatIsEquiv' a b f
  -
Monoid -> Monoid -> Type exact MonoidIsomorphism.
  -
forall a b : Monoid, (a $-> b) -> Type exact (fun M N f => IsEquiv f).
  -
forall a b : Monoid, MonoidIsomorphism a b -> a $-> b intros M N f; exact f.
  -
forall (a b : Monoid) (f : MonoidIsomorphism a b),
(fun (M N : Monoid) (f0 : M $-> N) => IsEquiv f0) a b
  ((fun (M N : Monoid) (f0 : MonoidIsomorphism M N) => mnd_iso_homo M N f0) a
     b f) cbn; exact _.
  -
forall (a b : Monoid) (f : a $-> b),
(fun (M N : Monoid) (f0 : M $-> N) => IsEquiv f0) a b f ->
MonoidIsomorphism a b exact Build_MonoidIsomorphism.
  -
forall (a b : Monoid) (f : a $-> b)
(fe : (fun (M N : Monoid) (f0 : M $-> N) => IsEquiv f0) a b f),
(fun (M N : Monoid) (f0 : MonoidIsomorphism M N) => mnd_iso_homo M N f0) a b
  {| mnd_iso_homo := f; isequiv_mnd_iso := fe |} $==
f reflexivity.
  -
forall a b : Monoid, MonoidIsomorphism a b -> b $-> a intros M N; exact mnd_iso_inverse.
  -
forall (a b : Monoid) (f : MonoidIsomorphism a b),
(fun (M N : Monoid) (x : MonoidIsomorphism M N) =>
 mnd_iso_homo N M (mnd_iso_inverse x)) a b f $o
(fun (M N : Monoid) (f0 : MonoidIsomorphism M N) => mnd_iso_homo M N f0) a b
  f $==
Id a intros ????; apply eissect.
  -
forall (a b : Monoid) (f : MonoidIsomorphism a b),
(fun (M N : Monoid) (f0 : MonoidIsomorphism M N) => mnd_iso_homo M N f0) a b
  f $o
(fun (M N : Monoid) (x : MonoidIsomorphism M N) =>
 mnd_iso_homo N M (mnd_iso_inverse x)) a b f $==
Id b intros ????; apply eisretr.
  -
forall (a b : Monoid) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> (fun (M N : Monoid) (f0 : M $-> N) => IsEquiv f0) a b f intros M N; exact isequiv_adjointify.
Defined.

Instance is0functor_monoid_type : Is0Functor monoid_type
  := Build_Is0Functor monoid_type (@mnd_homo_map).

Instance is1functor_monoid_type : Is1Functor monoid_type.
Is1Functor monoid_type
Proof.
Is1Functor monoid_type
  by apply Build_Is1Functor.
Defined.

(** ** Direct product of monoids *)

Definition mnd_prod : Monoid -> Monoid -> Monoid.
Monoid -> Monoid -> Monoid
Proof.
Monoid -> Monoid -> Monoid
  intros M N.
M, N: Monoid
Monoid
  snapply (Build_Monoid (M * N)).
M, N: Monoid
SgOp (M * N)
M, N: Monoid
MonUnit (M * N)
M, N: Monoid
IsMonoid (M * N)
  3: repeat split.
M, N: Monoid
SgOp (M * N)
M, N: Monoid
MonUnit (M * N)
M, N: Monoid
IsHSet (M * N)
M, N: Monoid
Associative sg_op
M, N: Monoid
LeftIdentity sg_op 1
M, N: Monoid
RightIdentity sg_op 1
  -
M, N: Monoid
SgOp (M * N) intros [m1 n1] [m2 n2].
M, N: Monoid
m1: M
n1: N
m2: M
n2: N
M * N
    exact (m1 * m2, n1 * n2).
  -
M, N: Monoid
MonUnit (M * N) exact (mon_unit, mon_unit).
  -
M, N: Monoid
IsHSet (M * N) exact _.
  -
M, N: Monoid
Associative sg_op intros x y z; snapply path_prod; napply mnd_assoc.
  -
M, N: Monoid
LeftIdentity sg_op 1 intros x; snapply path_prod; napply mnd_unit_l.
  -
M, N: Monoid
RightIdentity sg_op 1 intros x; snapply path_prod; napply mnd_unit_r.
Defined.

Definition mnd_prod_pr1 {M N : Monoid}
  : MonoidHomomorphism (mnd_prod M N) M.
M, N: Monoid
MonoidHomomorphism (mnd_prod M N) M
Proof.
M, N: Monoid
MonoidHomomorphism (mnd_prod M N) M
  snapply Build_MonoidHomomorphism.
M, N: Monoid
mnd_prod M N -> M
M, N: Monoid
IsMonoidPreserving ?mnd_homo_map
  1: exact fst.
M, N: Monoid
IsMonoidPreserving fst
  split; hnf; reflexivity.
Defined.

Definition mnd_prod_pr2 {M N : Monoid}
  : MonoidHomomorphism (mnd_prod M N) N.
M, N: Monoid
MonoidHomomorphism (mnd_prod M N) N
Proof.
M, N: Monoid
MonoidHomomorphism (mnd_prod M N) N
  snapply Build_MonoidHomomorphism.
M, N: Monoid
mnd_prod M N -> N
M, N: Monoid
IsMonoidPreserving ?mnd_homo_map
  1: exact snd.
M, N: Monoid
IsMonoidPreserving snd
  split; hnf; reflexivity.
Defined.

Definition mnd_prod_corec {M N P : Monoid}
  (f : MonoidHomomorphism P M)
  (g : MonoidHomomorphism P N)
  : MonoidHomomorphism P (mnd_prod M N).
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
MonoidHomomorphism P (mnd_prod M N)
Proof.
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
MonoidHomomorphism P (mnd_prod M N)
  snapply Build_MonoidHomomorphism.
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
P -> mnd_prod M N
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
IsMonoidPreserving ?mnd_homo_map
  2: split.
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
P -> mnd_prod M N
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
IsSemiGroupPreserving ?mnd_homo_map
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
IsUnitPreserving ?mnd_homo_map
  -
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
P -> mnd_prod M N exact (fun x => (f x, g x)).
  -
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
IsSemiGroupPreserving (fun x : P => (f x, g x)) intros x y; snapply path_prod; napply mnd_homo_op.
  -
M, N, P: Monoid
f: MonoidHomomorphism P M
g: MonoidHomomorphism P N
IsUnitPreserving (fun x : P => (f x, g x)) snapply path_prod; napply mnd_homo_unit.
Defined.

Instance hasbinaryproducts_monoid : HasBinaryProducts Monoid.
HasBinaryProducts Monoid
Proof.
HasBinaryProducts Monoid
  intros M N.
M, N: Monoid
BinaryProduct M N
  snapply Build_BinaryProduct.
M, N: Monoid
Monoid
M, N: Monoid
?cat_binprod' $-> M
M, N: Monoid
?cat_binprod' $-> N
M, N: Monoid
forall z : Monoid, (z $-> M) -> (z $-> N) -> z $-> ?cat_binprod'
M, N: Monoid
forall (z : Monoid) (f : z $-> M) (g : z $-> N),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
M, N: Monoid
forall (z : Monoid) (f : z $-> M) (g : z $-> N),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
M, N: Monoid
forall (z : Monoid) (f g : z $-> ?cat_binprod'),
?cat_pr1 $o f $== ?cat_pr1 $o g -> ?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
  -
M, N: Monoid
Monoid exact (mnd_prod M N).
  -
M, N: Monoid
mnd_prod M N $-> M exact mnd_prod_pr1.
  -
M, N: Monoid
mnd_prod M N $-> N exact mnd_prod_pr2.
  -
M, N: Monoid
forall z : Monoid, (z $-> M) -> (z $-> N) -> z $-> mnd_prod M N intros P; exact mnd_prod_corec.
  -
M, N: Monoid
forall (z : Monoid) (f : z $-> M) (g : z $-> N),
mnd_prod_pr1 $o (fun P : Monoid => mnd_prod_corec) z f g $== f intros P f g; exact (Id _).
  -
M, N: Monoid
forall (z : Monoid) (f : z $-> M) (g : z $-> N),
mnd_prod_pr2 $o (fun P : Monoid => mnd_prod_corec) z f g $== g intros P f g; exact (Id _).
  -
M, N: Monoid
forall (z : Monoid) (f g : z $-> mnd_prod M N),
mnd_prod_pr1 $o f $== mnd_prod_pr1 $o g ->
mnd_prod_pr2 $o f $== mnd_prod_pr2 $o g -> f $== g intros P f g p q a; exact (path_prod' (p a) (q a)).
Defined.