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. intro. induction p0. change (transportb _ _ _) with B1 in p1. induction p1. simpl. 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.