Definition cat_eq_1_to_cat_eq_2 (C D : precategory_data) (DS : ∏ (x y : D), isaset (precategory_morphisms x y)) : cat_eq_1 C D ≃ cat_eq_2 C D. Proof. use weqbandf. - use weqfibtototal. intro p. exact (data_cat_eq_1_to_2 C D p). - intros p. induction C as [C HC]. induction C as [CO CM]. induction HC as [CI CC]. induction D as [D HD]. induction D as [DO DM]. induction HD as [DI DC]. induction p as [p1 p2] ; cbn in *. unfold data_cat_eq_1 in p2. induction p1 ; cbn in *. induction p2 ; cbn. use weqdirprodf. + use weqimplimpl. * intros f a. induction f. reflexivity. * intros f. apply funextsec. intro z. apply f. * intro. apply impred_isaset. intro. apply DS. * apply impred. intro. apply DS. + use weqimplimpl. * intros p. induction p. reflexivity. * intros p. apply funextsec ; intro a. apply funextsec ; intro b. apply funextsec ; intro c. apply funextsec ; intro f. apply funextsec ; intro g. specialize (p a b c f g). induction p. reflexivity. * repeat (apply impred_isaset ; intro). apply DS. * repeat (apply impred ; intro). apply DS. 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.