Lemma eqweq_ob_path_is_functor_app {A B : precategory_data} (F : catiso A B) : forall a : A, eqweqmap (catiso_to_precategory_ob_path F) a = F a. Proof. intros a. exact (! toforallpaths (λ _ : A, B) F (pr1 (eqweqmap (invmap (univalence A B) (catiso_ob_weq F)))) (maponpaths pr1 (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a). 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.