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