{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).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions HFiber Truncations NullHomotopy Limits.Pullback. Require Import Descent Lex Separated.