Definition data_cat_eq_1_to_2 (C D : precategory_data) (Fo : (ob C) = ob D) : data_cat_eq_1 C D Fo ≃ data_cat_eq_2 C D Fo. Proof. induction C as [C HC]. induction C as [CO CM]. induction D as [D HD]. induction D as [DO DM]. cbn in *. induction Fo. unfold data_cat_eq_1, data_cat_eq_2. cbn. refine (_ ∘ weqtoforallpaths _ _ _)%weq. use weqonsecfibers. intros x. exact (weqtoforallpaths _ _ _)%weq. 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.