Definition cat_path_to_cat_eq_1 (C D : precategory_data) : C = D ≃ cat_eq_1 C D. Proof. refine (_ ∘ total2_paths_equiv _ _ _)%weq. use weqbandf. - apply total2_paths_equiv. - intro p ; cbn. induction C as [C HC]. induction D as [D HD]. cbn in *. induction p ; cbn. refine (_ ∘ total2_paths_equiv _ _ _)%weq. use weqfibtototal. intros p. cbn. rewrite transportf_const. exact (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.