proposition: Lemma is_preimage_for_pre_composition : functor_composite H GG = F.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering