fact: Definition O_indpaths (g h : O_reflector O P -> Q) (p : g o to O P == h o to O P) : g == h := (fst (snd (extendable_to_O O 2) g h) p).1.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout