Definition ind_weq : (∏ P : ∏ s : sorts σ, gterm σ s → UU, term_ind_HP P → ∏ (s : sorts σ) (t : gterm σ s), P s t) ≃ (∏ P : U → UU, ind_HP P → ∏ w : U, P w). Proof. use weqonsec. + exact lower_predicate. + intro P. use weqonsec. - use HP_weq. - intros H. cbn beta. use toLowerPredicateWeq. Defined.
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.