Definition path_setcategory (C D : setcategory) : C = D ≃ category_from_setcategory C = category_from_setcategory D. Proof. use weq_iso. - exact path_setcategory_help_fun. - intro p. use total2_paths_f. + exact (base_paths _ _ p). + apply isaprop_is_setcategory. - abstract (intro p ; induction p ; rewrite path_setcategory_help_fun_eq ; unfold path_setcategory_help_fun_alt ; rewrite base_total2_paths ; refine (_ @ total2_fiber_paths _) ; apply maponpaths ; apply isasetaprop ; apply isaprop_is_setcategory). - abstract (intro p ; induction C as [ C HC ] ; induction D as [ D HD ] ; rewrite path_setcategory_help_fun_eq ; unfold path_setcategory_help_fun_alt ; rewrite base_total2_paths ; refine (_ @ total2_fiber_paths _) ; apply maponpaths ; apply isasetaprop ; apply isaprop_has_homsets). Defined.
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.