Lemma k_transport (b : ob B) (c : ob C) (p : pr1 (pr1 t) = c) (a : ob A) (h : iso (pr1 H a) b): transportf (λ c' : ob C, ∏ a : ob A, iso (pr1 H a) b -> iso ((pr1 F) a) c') p (k) a h = (k b) b a h · idtoiso p .
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.