(** * Morphisms in a groupoid *)
Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Trunc Equivalences HoTT.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.


Local Open Scope category_scope.

Section groupoid_category.
  Variable X : Type.
  Context `{IsTrunc 1 X}.

  Definition isotoid (s d : groupoid_category X)
  : s <~=~> d -> s = d
    := fun f => f : morphism _ _ _.

  (** ** All groupoids are categories *)
  Global Instance iscategory_groupoid_category
  : IsCategory (groupoid_category X).
X: Type
IsTrunc0: IsTrunc 1 X
IsCategory (groupoid_category X)
  Proof.
X: Type
IsTrunc0: IsTrunc 1 X
IsCategory (groupoid_category X)
    repeat intro.
X: Type
IsTrunc0: IsTrunc 1 X
s, d: groupoid_category X
IsEquiv (idtoiso (groupoid_category X) (y:=d))
    apply (isequiv_adjointify (@idtoiso (groupoid_category X) _ _)
                              (@isotoid _ _));
      repeat intro;
      destruct_head @Isomorphic;
      destruct_head @IsIsomorphism;
      compute in *;
      path_induction_hammer.
  Qed.
End groupoid_category.