Lemma pdelta_preimage : pre_whisker H delta = gamma. Proof. apply nat_trans_eq. - apply C. - intro a. intermediate_path (pr1 (pr1 (iscontr_aux_space (H a)))). + apply idpath. + rewrite (pr2 (pr1 (iscontr_aux_space (H a))) a (identity_z_iso _)). rewrite z_iso_inv_of_z_iso_id. simpl. rewrite 2 functor_id. rewrite id_right. apply id_left. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. 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.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.