Definition weq_from_fully_faithful {C D : precategory_data}{F : functor C D} (FF : fully_faithful F) (a b : ob C) : (a --> b) ≃ (F a --> F b). Proof. exists (functor_on_morphisms F (a:=a) (b:=b)). exact (FF a b). 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.