Lemma catiso_to_precategory_data_path {A B : precategory} (F : catiso A B) : precategory_data_from_precategory A = precategory_data_from_precategory B. Proof. destruct A as [[[Ao Am] [Ai Ac]] Aax]. destruct B as [[[Bo Bm] [Bi Bc]] Bax]. eapply total2_paths_b. Unshelve. 2: { simpl. exact (catiso_to_precategory_ob_mor_path F). } apply pathsinv0. eapply pathscomp0. apply (transportb_dirprod _ _ _ _ _ (catiso_to_precategory_ob_mor_path F)). apply dirprodeq. - apply funextsec. intros a. apply (catiso_to_precategory_id_path F). - apply funextsec. intro. apply funextsec. intro. apply funextsec. intro. apply (catiso_to_precategory_comp_path F). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.