Theorem HP_weq : term_ind_HP P ≃ ind_HP (lowP). Proof. use weqonsecfibers. intro x. cbn beta. use weqonsec. + use gtweq_sec. + intro v. use weqonsec. - use ind_HP_Hypo. - intro HypOnSub. use ind_HP_Th. 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.