Lemma full_and_faithful_implies_fully_faithful (C D : precategory_data) (F : functor C D) : full_and_faithful F -> fully_faithful F. Proof. intros [Hfull Hfaith]. intros a b. simpl in *. apply isweqinclandsurj. - apply Hfaith. - apply Hfull. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.