fact: Definition transportf_dirprod' (A : UU) (B B' : A -> UU) (a a': A) (x: B a) (x': B' a) (p : a = a') : transportf (λ a, B a × B' a) p (x,, x') = make_dirprod (transportf (λ a, B a) p x) (transportf (λ a, B' a) p x').
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Induction.PolynomialFunctors UniMath.Induction.W.Core UniMath.Induction.W.Wtypes UniMath.Induction.FunctorAlgebras_legacy UniMath.Algebra.Universal.Signatures UniMath.Algebra.Universal.Algebras UniMath.Algebra.Universal.HVectors UniMath.Algebra.Universal.Terms