Definition cat_equiv_to_catiso (C D : precategory_data) : cat_equiv C D → catiso C D. Proof. intros F. use tpair. - use tpair. + use tpair. * exact (pr1(pr1 F)). * exact (pr2(pr1 F)). + split. * exact (pr1(pr2 F)). * exact (pr2(pr2 F)). - split. + intros a b. apply (pr2(pr1 F)). + apply (pr1(pr1 F)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.catiso.