Definition weq_cat_eq_cat_equiv (C D : precategory_data) : cat_eq_2 C D ≃ cat_equiv C D. Proof. use weqbandf. - use weqbandf. + apply univalence. + intros p. unfold data_cat_eq_2. use weqonsecfibers. intros x. use weqonsecfibers. intros y. apply univalence. - intros q. apply idweq. 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.