Lemma transportf_eta_unit' {P: (unit → UU) → UU} {a: unit → UU} (y: a tt) : transportf (λ x0 : unit → UU, x0 tt) (eta_unit' a) y = y. Proof. rewrite (transportf_funextfun (λ A:UU, A) _ _ (λ x : unit, unit_rect (λ x0 : unit, a tt = a x0) (idpath (a tt)) x) ). unfold unit_rect. rewrite idpath_transportf. apply idpath. 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.