fact: Definition plus_indpaths_beta {P Q : Type} `{In Meet Q} (g h : Plus P -> Q) (p : g o (to_plus P) == h o (to_plus P)) (x : P) : plus_indpaths g h p (to_plus P x) = p x := (fst (snd (ooextendable_plus 2%nat) g h) p).2 x.
imports: HoTT.Basics HoTT.Types Extensions HFiber Truncations NullHomotopy Limits.Pullback Descent Lex Separated