proposition: Lemma pdelta_preimage : pre_whisker H delta = gamma.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering