reflectsD_from_OO_ind@{i} {O' O : Subuniverse@{i}} {A : Type@{i}} `{PreReflects O' A} (OO_ind' : forall (B : O_reflector O' A -> Type@{i}) (B_inO : forall oa, In O (B oa)) (f : forall a, B (to O' A a)) oa, B oa) (OO_ind_beta' : forall (B : O_reflector O' A -> Type@{i}) (B_inO : forall oa, In O (B oa)) (f : forall a, B (to O' A a)) a, OO_ind' B B_inO f (to O' A a) = f a) (inO_paths' : forall (B : Type@{i}) (B_inO : In O B) (z z' : B), In O (z = z')) : ReflectsD O' O A. Proof. constructor. intros Q Q_inO n. revert Q Q_inO. simple_induction n n IHn; intros Q Q_inO. 1:exact tt. split. - intros g. exists (OO_ind' Q _ g). rapply OO_ind_beta'. - intros h k. rapply IHn. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.