{ f : forall a b, P a b & { e_a0 : forall b, f a0 b = f_a0 b & { e_b0 : forall a, f a b0 = f_b0 a & e_b0 a0 = (e_a0 b0) @ f_a0b0 }}}. Proof. assert (goal_as_extension : ExtensionAlong (unit_name a0) (fun a => ExtensionAlong (unit_name b0) (P a) (unit_name (f_b0 a))) (unit_name (f_a0 ; (unit_name f_a0b0)))). - apply (extension_conn_map_elim m). + apply (conn_point_incl a0). + intros a. apply (istrunc_extension_along_conn (n := n)). * apply (conn_point_incl b0). * apply HP. - destruct goal_as_extension as [f_eb name_ea_eab]. assert (ea_eab := name_ea_eab tt); clear name_ea_eab. exists (fun a => pr1 (f_eb a)). exists (fun b => apD10 (ea_eab ..1) b). exists (fun a => pr2 (f_eb a) tt). apply moveL_Mp. apply (concatR (apD10 (ea_eab ..2) tt)). set (ea := ea_eab ..1). generalize ea; simpl. clear ea_eab ea. intros. rewrite transport_arrow. rewrite transport_const. rewrite transport_paths_Fl. exact 1%path. Qed.
Require Import Basics. Require Import Types. Require Import Extensions. Require Import Factorization. Require Import Modalities.Descent. Require Import Truncations.Core Truncations.SeparatedTrunc.