Definition inv_weqonsecbase {X Y} {P:Y→UU} (f:X≃Y) {xz} {y} : invmap (weqonsecbase P f) xz y = transportf _ (homotweqinvweq f y) (xz (invmap f y)). Proof. 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.