(g h : O_reflector O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x := (fst (snd (extendable_to_O O 2) g h) p).
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.