Theorem UnderstandingR : R nm v = (invweq ((ind_HP_Th P nm v)))∘(e_s nm f)∘(ind_HP_Hypo P nm v). Proof. rewrite UnderstangHP_weq. change (invweq (HP_weq P) e_s nm v) with (invmap (HP_weq P) e_s nm v). unfold HP_weq. rewrite (inv_weqonsecfibers (P:=(λ x : names σ, ∏ v0 : (gterm σ)⋆ (arity x), hvec (h1map_vec P v0) → P (sort x) (build_gterm x v0))) (Q:=(λ x : names σ, ∏ f0 : B x → U, (∏ u : B x, lower_predicate P (f0 u)) → lower_predicate P (sup x f0)))). rewrite inv_weqonsec. rewrite inv_weqonsec. apply idpath. 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.