proposition: Lemma transport_comp_target {A0 B0 : UU} (p0 : A0 = B0) (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb (λ T, T -> T -> UU) p0 B1) : forall a a' a'' : A0, ( B1 (eqweqmap p0 a) (eqweqmap p0 a') -> B1 (eqweqmap p0 a') (eqweqmap p0 a'') -> B1 (eqweqmap p0 a) (eqweqmap p0 a'')) -> ( A1 a a' -> A1 a' a'' -> A1 a a'').
proof: Proof. intros a a' a''. intros Bhom. intros f g. set (X := λ a a', (transport_mor B1 p0 a a') @ (! weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a') ). apply (eqweqmap (X a a'')). apply Bhom. apply (eqweqmap (! X a a')). exact f. apply (eqweqmap (! X a' a'')). exact g. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful