proposition: Lemma iscontr_aux_space (b : B) : iscontr (total2 (fun g : F b --> G b => ∏ a : A, ∏ f : z_iso (H a) b, g = functor_on_z_iso F (z_iso_inv_from_z_iso f) · gamma a · #G f)).
proof: Proof. apply (p b (make_hProp _ (isapropiscontr _))). intro t; induction t as [anot h]; simpl. set (g := functor_on_z_iso F (z_iso_inv_from_z_iso h) · gamma anot · #G h). assert (gp : ∏ (a : A) (f : z_iso (H a) b), g = #F (inv_from_z_iso f) · gamma a · #G f). - intros a f. apply (Hf _ _ (h · inv_from_z_iso f) (make_hProp _ (homset_property C _ _ _ _))). intro sur. simpl. unfold g. rewrite functor_on_z_iso_inv; simpl. rewrite <- assoc. apply z_iso_inv_on_right. rewrite 2 assoc. simpl. rewrite <- functor_comp. rewrite <- (pr2 sur). simp_rew (nat_trans_ax gamma). rewrite (pr2 sur). rewrite <- assoc. apply cancel_precomposition. rewrite <- functor_comp. apply maponpaths. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply pathsinv0, id_right. - exists (g,, gp). intro t; induction t as [g' gp']. apply subtypePath. { intro; do 2 (apply impred; intro). apply C. } simpl. rewrite (gp anot h). rewrite (gp' anot h). apply idpath. 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