{A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) {C : Contr (sig R)} : IsIdentitySystem R r0. Proof. snrapply Build_IsIdentitySystem. - intros D d0 a r. exact (transport (fun ar : sig R => D (pr1 ar) (pr2 ar)) (path_contr (a0; r0) (a; r)) d0). - intros D d0; cbn; unfold path_contr. nrapply (transport2 _ (concat_Vp _)). Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.