(b:B) (v:Q b) : O (hfiber (functor_sigma f g) (b;v)) <~> O (hfiber f b). Proof. equiv_via (O {w : hfiber f b & hfiber (g w.1) ((w.2)^ # v)}). { apply equiv_O_functor, hfiber_functor_sigma. } equiv_via (O {w : hfiber f b & O (hfiber (g w.1) ((w.2)^ # v))}). { symmetry; apply equiv_O_sigma_O. } apply equiv_O_functor. apply equiv_sigma_contr; intros [a p]; simpl; exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.