(** * Morphisms in a groupoid *)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 *)X: Type
IsTrunc0: IsTrunc 1 XIsCategory (groupoid_category X)X: Type
IsTrunc0: IsTrunc 1 XIsCategory (groupoid_category X)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.X: Type
IsTrunc0: IsTrunc 1 X
s, d: groupoid_category XIsEquiv (idtoiso (groupoid_category X) (y:=d))