proposition: Lemma istrunc_extension_along_conn `{Funext} {m n : trunc_index} {A B : Type} (f : A -> B) `{IsConnMap n _ _ f} (P : B -> Type) {HP : forall b:B, IsTrunc (m +2+ n) (P b)} (d : forall a:A, P (f a)) : IsTrunc m (ExtensionAlong f P d).
proof: Proof. revert P HP d. simple_induction m m' IH; intros P HP d; simpl in *. - apply (Build_Contr _ (extension_conn_map_elim n f P d)). intros y. apply (allpath_extension_conn_map n); assumption. - apply istrunc_S. intros e e'. refine (istrunc_isequiv_istrunc _ (path_extension e e')). Defined.
imports: Basics Types Extensions Factorization Modalities.Modality Modalities.Descent Truncations.Core Truncations.SeparatedTrunc