proposition: Lemma path_precategory_uncurried'_idpath `{Funext} C : @path_precategory_uncurried' _ C C (idpath; (idpath; (idpath, idpath))) = idpath.
proof: Proof. destruct C; cbn in *. rewrite !(contr idpath). reflexivity. Qed.
imports: Category.Core HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Trunc HoTT.Basics.Tactics HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall HoTT.Tactics