Lemma eqweq_fully_faithful_is_functor_app {A B : precategory_data} (F : catiso A B) : forall a a' : A, eqweqmap (catiso_fully_faithful_path F a a') = catiso_fully_faithful_weq F _ _. Proof. intros a a'. unfold catiso_fully_faithful_path. assert (W := (@homotweqinvweq _ _ (univalence (a --> a') (F a --> F a')))). simpl in W. rewrite W. 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.