proposition: Lemma isweqtransportb10 { X : UU } ( P : X -> UU ) { x x' : X } ( e : x = x' ) : isweq ( transportb P e ).
proof: Proof. intros. apply ( isweqtransportf10 _ ( pathsinv0 e ) ). Defined.
imports: UniMath.Foundations.PartB