Lemma is_preimage_for_pre_composition : functor_composite H GG = F. Proof. apply (functor_eq _ _ C (functor_composite H GG) F). apply (total2_paths_f extphi). apply funextsec; intro a0; apply funextsec; intro a0'; apply funextsec; intro f. rewrite transport_of_functor_map_is_pointwise. unfold extphi. unfold double_transport. rewrite toforallpaths_funextsec. rewrite <- idtoiso_postcompose. rewrite <- idtoiso_precompose. rewrite idtoiso_inv. rewrite <- assoc. assert (PSIf : ∏ (a : A) (h : z_iso (H a) (H a0)) (a' : A) (h' : z_iso (H a') (H a0')) (l : a --> a'), #H l· h' = h· #H f -> #F l· k (H a0') a' h' = k (H a0) a h· ((idtoiso (phi a0)· #F f)· inv_from_z_iso (idtoiso (phi a0')))). { intros a h a' h' l alpha. rewrite assoc. apply z_iso_inv_on_left. unfold phi. repeat rewrite assoc. rewrite (Xkphi_idtoiso (H a0) (XtripleF a0)). repeat rewrite <- assoc. rewrite (Xkphi_idtoiso (H a0') (XtripleF a0')). simpl. assert (HH4 : fH^-1 h · f = l · fH^-1 h'). { apply (invmaponpathsweq (weq_from_fully_faithful fH a a0')). simpl; repeat rewrite functor_comp. inv_functor fH a a0. inv_functor fH a' a0'. apply pathsinv0, alpha. } intermediate_path (#F (fH^-1 h· f)). { rewrite functor_comp. apply idpath. } rewrite HH4. rewrite functor_comp. apply idpath. } set (Ybla := tpair _ (idtoiso (phi a0) · #F f · inv_from_z_iso (idtoiso (phi a0'))) PSIf : Y (#H f)). set (Ycontr := pr2 (Y_iscontr _ _ (#(pr1 H) f)) Ybla). set (Ycontr2 := base_paths _ _ Ycontr); simpl in *. change (G (#H f)) with (G (#(pr1 H) f)). rewrite <- Ycontr2. repeat rewrite assoc. rewrite z_iso_after_z_iso_inv, id_left. repeat rewrite <- assoc. rewrite z_iso_after_z_iso_inv, id_right. 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.