Theorem ind_HP_Th : P (sort nm) (build_gterm nm v) ≃ lowP (sup nm f). 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 comp_maponsecfibers. unfold gtweq_sectoU, weqbfun. simpl. rewrite (inv_weqonsecbase (P:=(λ _ : B nm → U, U)) (gtweq_sec nm)). *) 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.
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.