Lemma Y_inhab_proof (b b' : B) (f : b --> b') (a0 : A) (h0 : z_iso (H a0) b) (a0' : A) (h0' : z_iso (H a0') b') : ∏ (a : A) (h : z_iso (H a) b) (a' : A) (h' : z_iso (H a') b') (l : a --> a'), #H l· h' = h· f -> #F l· k b' a' h' = k b a h· ((inv_from_z_iso (k b a0 h0)· #F (fH^-1 ((h0· f)· inv_from_z_iso h0')))· k b' a0' h0'). Proof. intros a h a' h' l alpha. set (m := fH^-i (z_iso_comp h0 (z_iso_inv_from_z_iso h))). set (m' := fH^-i (z_iso_comp h0' (z_iso_inv_from_z_iso h'))). assert (sss : z_iso_comp (functor_on_z_iso F m) (k b a h) = k b a0 h0). { apply z_iso_eq. apply (q b (tpair _ a0 h0) (tpair _ a h) m). simpl. inv_functor fH a0 a. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } assert (ssss : z_iso_comp (functor_on_z_iso F m') (k b' a' h') = k b' a0' h0'). { apply z_iso_eq. apply (q b' (tpair _ a0' h0') (tpair _ a' h') m'). simpl; inv_functor fH a0' a'. rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. } set (hfh := h0 · f · inv_from_z_iso h0'). set (l0 := fH^-1 hfh). set (g0 := inv_from_z_iso (k b a0 h0) · #F l0 · k b' a0' h0'). assert (sssss : #H (l0 · m') = #H (m · l)). { rewrite functor_comp . unfold m'. simpl. inv_functor fH a0' a'. unfold l0. inv_functor fH a0 a0'. unfold hfh. intermediate_path (h0 · f · (inv_from_z_iso h0' · h0') · inv_from_z_iso h'). { repeat rewrite assoc; apply idpath. } rewrite z_iso_after_z_iso_inv, id_right, functor_comp. inv_functor fH a0 a. repeat rewrite <- assoc. apply maponpaths, pathsinv0, z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left, pathsinv0, alpha. } assert (star5 : inv_from_z_iso m · l0 = l · inv_from_z_iso m'). { apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left, (invmaponpathsweq (weq_from_fully_faithful fH a0 a' )), pathsinv0, sssss. } clear sssss. unfold g0. assert (sss'' : k b a h · inv_from_z_iso (k b a0 h0) = inv_from_z_iso (functor_on_z_iso F m)). { apply pathsinv0, z_iso_inv_on_left, pathsinv0. apply z_iso_inv_on_right. unfold m; simpl. apply pathsinv0, (base_paths _ _ sss). } repeat rewrite assoc. rewrite sss''. clear sss'' sss. rewrite <- functor_on_inv_from_z_iso. rewrite <- functor_comp. rewrite star5; clear star5. rewrite functor_comp, functor_on_inv_from_z_iso. assert (star4 : inv_from_z_iso (functor_on_z_iso F m')· k b' a0' h0' = k b' a' h' ). { apply z_iso_inv_on_right. apply pathsinv0, (base_paths _ _ ssss). } rewrite <- assoc. rewrite star4. apply idpath. Qed.
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.