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. 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.
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.