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