Proposition path_setcategory_help_fun_eq {C D : setcategory} (p : C = D) : path_setcategory_help_fun p = path_setcategory_help_fun_alt p. Proof. induction p. refine (!_). refine (_ @ total2_fiber_paths _). unfold path_setcategory_help_fun_alt. apply maponpaths. apply isasetaprop. apply isaprop_has_homsets. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.CategoryEquality. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Section FromIso. End FromIso.