proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful