Lemma fully_faithful_from_equivalence : fully_faithful F. Proof. unfold fully_faithful. intros a b. apply (isweq_iso _ (@inverse a b)). - apply inverse_is_inverse_1. - apply inverse_is_inverse_2. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core.