Definition kFa (a0 : A) : ∏ a : A, z_iso (H a) (H a0) -> z_iso (F a) (F a0) := fun (a : A) (h : z_iso (H a) (H a0)) => functor_on_z_iso F (iso_from_fully_faithful_reflection fH h).
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.