fact: Definition O_ind2paths_beta {g h : O_reflector O P -> Q} (p q : g == h) (r : p oD (to O P) == q oD (to O P)) (x : P) : O_ind2paths p q r (to O P x) = r x := (fst (snd (snd (extendable_to_O O 3) g h) p q) r).2 x.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout