Definition catiso_to_cat_equiv (C D : precategory_data) : catiso C D → cat_equiv C D. Proof. intros F. use tpair. - use tpair. + use make_weq. * exact (functor_on_objects F). * apply F. + intros a b. use make_weq. * exact (functor_on_morphisms F). * apply F. - split. + exact (functor_id F). + exact (@functor_comp _ _ 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.