Definition inv_weqonsecfibers {X : UU} {P Q : X → UU} (f : (∏ x : X, (P x ≃ Q x))) : invmap (weqonsecfibers P Q f) = (λ q x, invmap (f x) (q x)). Proof. use funextsec. intro q. use funextsec. intro x. use maponpaths. simpl. use proofirrelevance. fold ((hfiber (f x) (q x))). use isapropifcontr. use weqproperty. 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.