proposition: Lemma transportb_fun {P: (unit → UU) → UU} {Q: (unit → UU) → UU} {a a': unit → UU} {p: a = a'} {f: P a' → Q a'} {x: P a} : transportb (λ x: unit → UU, P x → Q x) p f x = transportb (λ x: unit → UU, Q x) p (f (transportf (λ x: unit → UU, P x) p x)).
proof: Proof. induction p. apply idpath. Qed.
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