(n : nat) {A B : Type} (C : B -> Type) (f : A -> B) (ext : ExtendableAlong n f C) (D : forall b, C b -> Type) (g : forall b c, D b c) (ext' : ExtendableAlong_Over n f C D ext) {struct n} : Type. Proof. destruct n. - exact Unit. - apply prod. + exact (forall (h : forall a, C (f a)) (b : B), g b ((fst ext h).1 b) = (fst ext' h (fun a => g (f a) (h a))).1 b). + exact (forall h k, n A B (fun b => h b = k b) f (snd ext h k) (fun b c => c # g b (h b) = g b (k b)) (fun b c => apD (g b) c) (snd ext' h k _ _)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions. Require Import ReflectiveSubuniverse Accessible. Import IsLocal_Internal.