Lemma correct_hom_on_comp {A B : precategory} (F : catiso A B) : forall a a' a'', forall f : F a --> F a', forall g : F a' --> F a'', (eqweqmap (correct_hom F _ _)) f · (eqweqmap (correct_hom F _ _)) g = (eqweqmap (correct_hom F _ _)) (f · g). Proof. intros a a' a'' f g. rewrite !eqweq_correct_hom_is_comp. induction (eqweq_ob_path_is_functor_app F a). induction (eqweq_ob_path_is_functor_app F a'). induction (eqweq_ob_path_is_functor_app F a''). rewrite 3 id_left. simpl. rewrite 3 id_right. 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.