GrpCategory.v

Require Import Groups.Group.
Require Import Category Categories.Structure Categories.SetCategory.

(** * The (univalent) category of groups *)

Record GroupStructure (A : hSet) := {
  gp_sgop : SgOp A;
  gp_unit : MonUnit A;
  gp_inverse : Negate A;
  gp_isgroup : IsGroup A;
}.

Definition issig_GroupStructure {A : hSet}
  : _ <~> GroupStructure A := ltac:(issig).

Definition group_structure `{Funext} : NotionOfStructure set_cat.
Proof.
  srapply Build_NotionOfStructure.
  (* Groups are sets with a GroupStructure, as defined above. *)
  1: exact GroupStructure. 
  (* The notion of homomorphism is given by IsMonoidPreserving. *)
  1: intros ? ? f [?] [?]; rapply (IsMonoidPreserving f). 
  (* (IsMonoidPreserving f) is an HProp and idmap is a homomorphism. *)
  1,2: cbn; intros; exact _.
  (* Homomorphisms may be composed. *)
  cbn; intros; rapply (compose_monoid_morphism _ _ _ _); eassumption.
Defined.

Instance isstandard_group_structure `{Univalence}
  : IsStandardNotionOfStructure group_structure.
Proof.
  intros A [?] [?] [sgmor0 pmor0] [?].
  apply (equiv_ap_inv' issig_GroupStructure); cbn.
  apply equiv_path_sigma.
  srefine (_;_); cbn.
  1: funext x y; apply sgmor0.
  refine (transport_sigma' _ _ @ _).
  apply equiv_path_sigma; cbn.
  srefine (_;_).
  1: apply pmor0.
  refine (transport_sigma' _ _ @ _).
  apply equiv_path_sigma_hprop; cbn.
  refine (ap pr1 (transport_sigma' _ _) @ _); cbn.
  funext x.
  rapply (preserves_negate (f:=idmap) x).
  1,2: exact _. (* jarlg: May not find the correct group structures? *)
  rapply Build_IsMonoidPreserving.
Defined.

Definition Gp `{Univalence} : PreCategory := precategory_of_structures group_structure.

Global Instance iscategory_group `{Univalence} : IsCategory Gp := _.

Theorem equiv_path_group' `{u : Univalence} (G H : Gp)
  : (G = H) <~> Isomorphic G H.
Proof.
  srapply Build_Equiv.
  - apply idtoiso.
  - exact _.
Defined.