Lemma weq_ff_functor_on_weq_isobandf_compute {C D : category} (F : functor C D) (HF : fully_faithful F) {a b : C} (f : z_iso a b) : #F f = weq_ff_functor_on_weq_isobandf HF _ _ f. Proof. apply idpath. 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.