{A : Type} {a0 : A} (R : A -> Type) (r0 : R a0) `{!IsIdentitySystem _ r0} (a : A) : (a0 = a) <~> R a := Build_Equiv _ _ (fun p => transport R p r0) _.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.