Definition inv_weqonsec {X Y} {P:X->Type} {Q:Y->Type} {f:X ≃ Y} {g:∏ x, weq (P x) (Q (f x))} : (invmap (weqonsec P Q f g)) = (λ yq x, invmap (g x) (yq ( f x)) ). Proof. use funextsec. intro yq. use funextsec. intro x. unfold weqonsec. rewrite invmap_weqcomp_expand. simpl. rewrite inv_weqonsecfibers. 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.