(** * Groupoids *)
Require Import Category.Morphisms Category.Strict.
Require Import Trunc PathGroupoids Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.
Local Open Scope category_scope.

(** A groupoid is a precategory where every morphism is an isomorphism.  Since 1-types are 1-groupoids, we can construct the category corresponding to the 1-groupoid of a 1-type. *)

(** ** Definition of what it means to be a groupoid *)
Class IsGroupoid (C : PreCategory)
  := isgroupoid : forall s d (m : morphism C s d),
                    IsIsomorphism m.

Instance trunc_isgroupoid `{Funext} C : IsHProp (IsGroupoid C)
  := istrunc_forall.

(** We don't want access to all of the internals of a groupoid category at top level. *)
Module GroupoidCategoryInternals.
  Section groupoid_category.
    Variable X : Type.
    Context `{IsTrunc 1 X}.

    Local Notation morphism := (@paths X).

    Definition compose s d d' (m : morphism d d') (m' : morphism s d)
    : morphism s d'
      := transitivity m' m.

    Definition identity x : morphism x x
      := reflexivity _.

    Global Arguments compose [s d d'] m m' / .
    Global Arguments identity x / .
  End groupoid_category.
End GroupoidCategoryInternals.

(** ** Categorification of the groupoid of a 1-type *)
Definition groupoid_category X `{IsTrunc 1 X} : PreCategory.
X: Type
IsTrunc0: IsTrunc 1 X
PreCategory
Proof.
X: Type
IsTrunc0: IsTrunc 1 X
PreCategory
  refine (@Build_PreCategory X
                             (@paths X)
                             (@GroupoidCategoryInternals.identity X)
                             (@GroupoidCategoryInternals.compose X)
                             _
                             _
                             _
                             _);
  simpl; intros; path_induction; reflexivity.
Defined.

Arguments groupoid_category X {_}.

Instance isgroupoid_groupoid_category X `{IsTrunc 1 X}
: IsGroupoid (groupoid_category X).
X: Type
IsTrunc0: IsTrunc 1 X
IsGroupoid (groupoid_category X)
 Proof.
X: Type
IsTrunc0: IsTrunc 1 X
IsGroupoid (groupoid_category X)
  intros s d m; simpl in *.
X: Type
IsTrunc0: IsTrunc 1 X
s, d: X
m: s = d
IsIsomorphism m
  exact (Build_IsIsomorphism
           (groupoid_category X)
           s d
           m m^%path
           (concat_pV m)
           (concat_Vp m)).
Defined.

(** ** 0-types give rise to strict (groupoid) categories *)
Lemma isstrict_groupoid_category X `{IsHSet X}
: IsStrictCategory (groupoid_category X).
X: Type
IsHSet0: IsHSet X
IsStrictCategory (groupoid_category X)
Proof.
X: Type
IsHSet0: IsHSet X
IsStrictCategory (groupoid_category X)
  typeclasses eauto.
Defined.