proposition: Lemma transport_id {A0 B0 : UU} (p0 : A0 = B0) (A1 : A0 -> A0 -> UU) (B1 : B0 -> B0 -> UU) (p1 : A1 = transportb _ p0 B1) (idB : forall b : B0, B1 b b) : forall a : A0, (transportb (X := total2 (λ T, T -> T -> UU)) (λ T, forall a, (pr2 T) a a) (total2_paths2_b p0 p1) idB) a = (eqweqmap ( (transport_mor B1 p0 _ _) @ !weqtoforallpaths _ _ _ (weqtoforallpaths _ _ _ p1 a) a)) (idB (eqweqmap p0 a)).
proof: Proof. intro. induction p0. change (transportb _ _ _) with B1 in p1. induction p1. simpl. reflexivity. 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