proposition: Proposition path_setcategory_help_fun_eq {C D : setcategory} (p : C = D) : path_setcategory_help_fun p = path_setcategory_help_fun_alt p.
proof: Proof. induction p. refine (!_). refine (_ @ total2_fiber_paths _). unfold path_setcategory_help_fun_alt. apply maponpaths. apply isasetaprop. apply isaprop_has_homsets. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.CategoryEquality