Definition istranspathshrel (X : UU) : istrans (pathshrel X) := λ x x' x'' : _, λ a : _, λ b : _, hinhfun2 (fun e1 : x = x' => fun e2 : x' = x'' => e1 @ e2) a b.
Require Import UniMath.Foundations.UnivalenceAxiom.