proposition: Theorem ind_HP_Th : P (sort nm) (build_gterm nm v) ≃ lowP (sup nm f).
proof: Proof. change (sort nm) with tt. change (lowP) with (P tt). use eqweqmap. use maponpaths. unfold sup. unfold gtweqtoU. change (build_gterm nm v = transportf (λ _ : B nm → U, U) (homotweqinvweq (gtweq_sec nm) f) (build_gterm nm (invmap (gtweq_sec nm) f))). rewrite transportf_const. induction ((homotweqinvweq (gtweq_sec nm) f)). use pathsinv0. etrans. { use idpath_transportf. } use maponpaths. induction (!homotweqinvweq (gtweq_sec nm) f). use pathsinv0. use homotinvweqweq0. Defined.
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