fact: Definition plus_rec_beta {P Q : Type} `{In Meet Q} (f : P -> Q) (x : P) : plus_rec f (to_plus P x) = f x := (fst (ooextendable_plus 1%nat) f).2 x.
imports: HoTT.Basics HoTT.Types Extensions HFiber Truncations NullHomotopy Limits.Pullback Descent Lex Separated