Lemma eqweq_correct_hom_is_comp {A B : precategory} (F : catiso A B) : forall a a' : A, forall f : F a --> F a', eqweqmap (correct_hom F _ _) f = (idtomor _ _ (eqweq_ob_path_is_functor_app F a)) · f · (idtomor _ _ (!eqweq_ob_path_is_functor_app F a')). Proof. intros a a' f. rewrite (eqweq_maponpaths_mor _ _ (! homotweqinvweq (univalence A B) (catiso_ob_weq F)) a a'). apply maponpaths. apply maponpaths. unfold eqweq_ob_path_is_functor_app. rewrite pathsinv0inv0. reflexivity. 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.