proposition: Lemma eqweq_ob_path_is_functor_app_compute (A B : precategory) (F : catiso A B) (a a' : A) (f : B ⟦ F a, F a' ⟧): eqweq_ob_path_is_functor_app F a = ! toforallpaths (λ _ : A, B) F (pr1weq (eqweqmap (invmap (univalence A B) (catiso_ob_weq F)))) (maponpaths pr1weq (! homotweqinvweq (univalence A B) (catiso_ob_weq F))) a.
proof: Proof. unfold eqweq_ob_path_is_functor_app. Abort. Lemma eqweq_maponpaths_mor {A B : precategory} (F G : A ≃ B) (p : F = G) (a a' : A) (f : F a --> F a') : eqweqmap (maponpaths (λ T : A ≃ B, (pr1 T) a --> (pr1 T) a') p) f = (idtomor _ _ (!toforallpaths _ _ _ (maponpaths pr1 p) a)) · f · (idtomor _ _ (toforallpaths _ _ _ (maponpaths pr1 p) a')). Proof. induction p. rewrite id_left. rewrite id_right. 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