proposition: Lemma function : forall u v, hexists (fun w => forall x, x ∈ w <-> V_is_func u v x).
proof: Proof. intros u v. apply tr; exists (V_func u v). assert (memb_u : u = set (@func_of_members u)) by exact (is_valid_presentation u). assert (memb_v : v = set (@func_of_members v)) by exact (is_valid_presentation v). intro phi; split. - intro H. split;[split|]. + intros z Hz. simpl in *. generalize H. apply Trunc_rec. intros [h p_phi]. generalize (transport (fun x => z ∈ x) p_phi^ Hz). apply (Trunc_functor (-1)). intros [a p]. exists (a, h a). assumption. + intros x Hx. generalize (transport (fun y => x ∈ y) memb_u Hx). apply Trunc_rec. intros [a p]. generalize H; apply (Trunc_functor (-1)). intros [h p_phi]. exists (func_of_members (h a)). split. * exact (transport (fun z => func_of_members (h a) ∈ z) memb_v^ (tr (h a; 1))). * apply (transport (fun y => [x, func_of_members (h a)] ∈ y) p_phi). apply tr; exists a. rewrite p; reflexivity. + intros x y y' (Hy, Hy'). generalize H; apply Trunc_rec. intros [h p_phi]. generalize (transport (fun z => [x, y] ∈ z) p_phi^ Hy). apply Trunc_rec. intros [a p]. generalize (transport (fun z => [x, y'] ∈ z) p_phi^ Hy'). apply Trunc_rec. intros [a' p']. destruct (fst path_pair_ord p) as (px, py). destruct (fst path_pair_ord p') as (px', py'). transitivity (func_of_members (h a)); auto with path_hints. transitivity (func_of_members (h a'));auto with path_hints. refine (ap func_of_members _). refine (ap h _). apply (isinj_embedding func_of_members IsEmbedding_funcofmembers a a' (px @ px'^)). - intros ((H1, H2), H3). simpl. assert (h : forall a : [u], {b : [v] & [func_of_members a, func_of_members b] ∈ phi}). { intro a. pose (x := func_of_members a). transparent assert (H : {y : V & y ∈ v * [x, y] ∈ phi}). - refine (@untrunc_istrunc (-1) {y : V & y ∈ v * [x, y] ∈ phi} _ (H2 x (transport (fun z => x ∈ z) memb_u^ (tr (a; 1))))). apply hprop_allpath. intros [y (H1_y, H2_y)] [y' (H1_y', H2_y')]. apply path_sigma_uncurried; simpl. exists (H3 x y y' (H2_y, H2_y')). apply path_ishprop. - destruct H as [y (H1_y, H2_y)]. destruct (@untrunc_istrunc (-1) _ (IsEmbedding_funcofmembers y) (transport (fun z => y ∈ z) memb_v H1_y)) as [b Hb]. exists b. exact (transport (fun z => [x, z] ∈ phi) Hb^ H2_y). } apply tr; exists (fun a => pr1 (h a)). apply extensionality. split. + intros z Hz. generalize Hz; apply Trunc_rec. intros [a Ha]. exact (transport (fun w => w ∈ phi) Ha (pr2 (h a))). + intros z Hz. simpl. generalize (H1 z Hz). apply (Trunc_functor (-1)). intros [(a,b) p]. simpl in p. exists a. transitivity ([func_of_members a, func_of_members b]); auto with path_hints. apply ap. apply H3 with (func_of_members a). split. * exact (pr2 (h a)). * exact (transport (fun w => w ∈ phi) p^ Hz). Qed.
imports: HoTT.Basics HoTT.Types HSet TruncType Colimits.SpanPushout HoTT.Truncations.Core Colimits.Quotient