proposition: Lemma transportb_eta_unit'{P: (unit → UU) → UU} {a: unit → UU} (y: a tt) : transportb (λ x0 : unit → UU, x0 tt) (eta_unit' a) y = y.
proof: Proof. apply (transportb_transpose_left(P:= λ x0: unit → UU, x0 tt)(e:=eta_unit' a)). apply pathsinv0. apply (transportf_eta_unit'(P:= λ x0: unit → UU, x0 tt)). 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