Lemma fully_faithful_implies_full_and_faithful (C D : precategory_data) (F : functor C D) : fully_faithful F -> full_and_faithful F. Proof. intro H. split; simpl. unfold full. intros a b. apply issurjectiveweq. apply H. intros a b. apply isinclweq. apply H. Qed.
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.