Lemma transport_comp {A0 B0 : UU} (p0 : A0 = B0) (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb _ p0 B1) (compB : forall b b' b'' : B0, B1 b b' -> B1 b' b'' -> B1 b b'') : forall a a' a'' : A0, (transportb (X := total2 (λ T, T -> T -> UU)) (λ T, forall a b c, (pr2 T) a b -> (pr2 T) b c -> (pr2 T) a c) (total2_paths2_b p0 p1) compB) a a' a'' = transport_comp_target p0 A1 B1 p1 a a' a'' (compB (eqweqmap p0 a) (eqweqmap p0 a') (eqweqmap p0 a'')). Proof. intros. induction p0. change (A1 = B1) in p1. induction p1. reflexivity. 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.