(b:B) : hfiber (factor2 fact) b <~> hfiber (factor2 fact') b. Proof. refine (O_hfiber_O_fact fact' b oE _). refine (_ oE (O_hfiber_O_fact fact b)^-1). apply equiv_O_functor. apply equiv_hfiber_homotopic. exact H. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.