fact: Definition paths_pathsdirprod {X Y : UU} {x₁ x₂ : X} {y₁ y₂ : Y} {p₁ p₂ : x₁ = x₂} {q₁ q₂ : y₁ = y₂} (r₁ : p₁ = p₂) (r₂ : q₁ = q₂) : pathsdirprod p₁ q₁ = pathsdirprod p₂ q₂.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics