Lemma functor_from_equivalence_is_essentially_surjective : essentially_surjective F. Proof. unfold essentially_surjective. intros b; apply hinhpr. exists (G b). apply counit_pointwise_z_iso_from_adj_equivalence. Defined.
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.