Lemma is_nat_trans_pdelta : is_nat_trans F G pdelta. Proof. intros b b' f. apply (p b (make_hProp _ (homset_property C _ _ _ _) )). intro t; induction t as [a h]; simpl. apply (p b' (make_hProp _ (homset_property C _ _ _ _) )). intro t; induction t as [a' h']; simpl. unfold pdelta. rewrite (pr2 ((pr1 (iscontr_aux_space b))) a h). rewrite (pr2 ((pr1 (iscontr_aux_space b'))) a' h'). rewrite <- 3 assoc. apply pathsinv0. rewrite functor_on_z_iso_inv. apply z_iso_inv_on_right. rewrite 4 assoc. simpl. rewrite <- 2 functor_comp. apply (Hf _ _ (h · f · (inv_from_z_iso h')) (make_hProp _ (homset_property C _ _ _ _))). intro sur. simpl. rewrite <- (pr2 sur). simp_rew (nat_trans_ax gamma). rewrite (pr2 sur). rewrite <- 3 assoc. rewrite <- 2 functor_comp. apply cancel_precomposition, maponpaths. rewrite <- 2 assoc. rewrite z_iso_after_z_iso_inv. rewrite id_right. apply idpath. 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.