Lemma qF (a0 : A) : ∏ (t t' : total2 (λ a : A, z_iso (H a) (H a0))) (f : pr1 t --> pr1 t'), #H f· pr2 t' = pr2 t -> #F f· #F (fH^-1 (pr2 t')) = #F (fH^-1 (pr2 t)). Proof. simpl. intros [a h] [a' h'] f L. simpl in L; simpl. rewrite <- functor_comp. apply maponpaths. apply (invmaponpathsweq (weq_from_fully_faithful fH a a0) (f· fH^-1 h') (fH^-1 h) ). inv_functor fH a a0. rewrite functor_comp. inv_functor fH a' a0. apply L. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.