proposition: Corollary isweqweqtransportbUAH ( P : UU -> UU ) ( R : ∏ ( X X' : UU ) ( w : X ≃ X' ) , P X' -> P X ) ( r : ∏ X : UU , ∏ p : P X , R X X ( idweq X ) p = p ) : ∏ ( X X' : UU ) ( w : X ≃ X' ), isweq ( λ p' : P X', R X X' w p' ).
proof: Proof. intros. assert ( e : R X X' w ~ transportb P ( weqtopathsUAH w )). - unfold homot. apply weqtransportbUAH. assumption. - assert ( ee : transportb P ( weqtopathsUAH w ) ~ R X X' w). + intro p'. apply ( pathsinv0 ( e p' ) ). + clear e. assert ( is1 : isweq ( transportb P ( weqtopathsUAH w ) ) ). apply isweqtransportb10. apply ( isweqhomot ( transportb P ( weqtopathsUAH w ) ) (R X X' w) ee is1 ). Defined.
imports: UniMath.Foundations.PartB