fact: Fixpoint ExtendableAlong_Over@{a b c d m | a <= m, b <= m, c <= m, d <= m} (n : nat) {A : Type@{a}} {B : Type@{b}} (f : A -> B) (C : B -> Type@{c}) (D : forall b, C b -> Type@{d}) (ext : ExtendableAlong@{a b c m} n f C) : Type@{m} := match n return ExtendableAlong@{a b c m} n f C -> Type@{m} with | 0 => fun _ => Unit | S n => fun ext' => (forall (g : forall a, C (f a)) (g' : forall a, D (f a) (g a)), sig@{m m} (fun (rec : forall b, D b ((fst ext' g).1 b)) => forall a, (fst ext' g).2 a # rec (f a) = g' a )) * forall (h k : forall b, C b) (h' : forall b, D b (h b)) (k' : forall b, D b (k b)), ExtendableAlong_Over n f (fun b => h b = k b) (fun b c => c # h' b = k' b) (snd ext' h k) end ext.
imports: HoTT.Basics HoTT.Types Extensions ReflectiveSubuniverse Accessible