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').
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Induction.PolynomialFunctors. Require Import UniMath.Induction.W.Core. Require Import UniMath.Induction.W.Wtypes. Require Import UniMath.Induction.FunctorAlgebras_legacy. Require Import UniMath.Algebra.Universal.Signatures. Require Import UniMath.Algebra.Universal.Algebras. Require Import UniMath.Algebra.Universal.HVectors. Require Import UniMath.Algebra.Universal.Terms.