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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.All. 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.Core.Setcategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.