Timings for V.v
(* -*- mode: coq; mode: visual-line -*- *)
(** * The cumulative hierarchy [V]. *)
Require Import HoTT.Basics HoTT.Types.
Require Import HSet TruncType.
Require Import Colimits.SpanPushout.
Require Import HoTT.Truncations.Core Colimits.Quotient.
Local Open Scope nat_scope.
Local Open Scope path_scope.
Definition bitotal {A B : Type} (R : A -> B -> HProp) :=
(forall a : A, hexists (fun (b : B) => R a b))
* (forall b : B, hexists (fun (a : A) => R a b)).
(** ** The cumulative hierarchy V *)
Module Export CumulativeHierarchy.
Private Inductive V@{U' U | U < U'} : Type@{U'} :=
| set {A : Type@{U}} (f : A -> V) : V.
Axiom setext : forall {A B : Type} (R : A -> B -> HProp)
(bitot_R : bitotal R) (h : SPushout R -> V),
set (h o (spushl R)) = set (h o (spushr R)).
Axiom ishset_V : IsHSet V.
Global Existing Instance ishset_V.
(** The induction principle. Annotating the universes here greatly reduces the number of universe variables later in the file. For example, [function] below went from 279 to 3. If [V_ind] needs to be generalized in the future, check [function] to make sure things haven't exploded again. *)
Fixpoint V_ind@{U' U u | U < U'} (P : V@{U' U} -> Type@{u})
(H_0trunc : forall v : V@{U' U}, IsTrunc 0 (P v))
(H_set : forall (A : Type@{U}) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f))
(H_setext : forall (A B : Type@{U}) (R : A -> B -> HProp@{U}) (bitot_R : bitotal R)
(h : SPushout R -> V) (H_h : forall x : SPushout R, P (h x)),
transport@{U' u} _ (setext R bitot_R h) (H_set A (h o spushl R) (H_h oD spushl R))
= H_set B (h o spushr R) (H_h oD spushr R) )
(v : V)
: P v
:= (match v with
| set A f => fun _ _ => H_set A f (fun a => V_ind P H_0trunc H_set H_setext (f a))
end) H_setext H_0trunc.
(** We don't need to axiomatize the computation rule because we get it for free thanks to 0-truncation *)
Definition V_comp_setext (P : V -> Type)
(H_0trunc : forall v : V, IsTrunc 0 (P v))
(H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f))
(H_setext : forall (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R)
(h : SPushout R -> V) (H_h : forall x : SPushout R, P (h x)),
(setext R bitot_R h) # (H_set A (h o spushl R) (H_h oD spushl R))
= H_set B (h o spushr R) (H_h oD spushr R) )
(A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V)
: apD (V_ind P H_0trunc H_set H_setext) (setext R bitot_R h)
= H_setext A B R bitot_R h ((V_ind P H_0trunc H_set H_setext) oD h).
(** The non-dependent eliminator *)
Definition V_rec (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : forall (A : Type), (A -> V) -> (A -> P) -> P)
(H_setext : forall (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R)
(h : SPushout R -> V) (H_h : SPushout R -> P),
H_set A (h o spushl R) (H_h o spushl R) = H_set B (h o spushr R) (H_h o spushr R) )
: V -> P.
refine (V_ind _ _ H_set _).
exact (transport_const _ _ @ H_setext A B R bitot_R h H_h).
Definition V_comp_nd_setext (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : forall (A : Type), (A -> V) -> (A -> P) -> P)
(H_setext : forall (A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R)
(h : SPushout R -> V) (H_h : SPushout R -> P),
H_set A (h o spushl R) (H_h o spushl R) = H_set B (h o spushr R) (H_h o spushr R) )
(A B : Type) (R : A -> B -> HProp) (bitot_R : bitotal R) (h : SPushout R -> V)
: ap (V_rec P H_0trunc H_set H_setext) (setext R bitot_R h)
= H_setext A B R bitot_R h ((V_rec P H_0trunc H_set H_setext) o h).
(** ** Alternative induction principle (This is close to the one from the book) *)
Definition equal_img {A B C : Type} (f : A -> C) (g : B -> C) :=
(forall a : A, hexists (fun (b : B) => f a = g b))
* (forall b : B, hexists (fun (a : A) => f a = g b)).
Definition setext' {A B : Type} (f : A -> V) (g : B -> V) (eq_img : equal_img f g)
: set f = set g.
pose (R := fun a b => Build_HProp (f a = g b)).
pose (h := SPushout_rec R V f g (fun _ _ r => r)).
exact (setext R eq_img h).
Definition V_rec' (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : forall (A : Type), (A -> V) -> (A -> P) -> P)
(H_setext' : forall (A B : Type) (f : A -> V) (g : B -> V), (equal_img f g) ->
forall (H_f : A -> P) (H_g : B -> P), (equal_img H_f H_g) ->
(H_set A f H_f) = (H_set B g H_g) )
: V -> P.
refine (V_rec _ _ H_set _).
intros A B R bitot_R h H_h.
generalize (fst bitot_R a).
apply (Trunc_functor (-1)).
exact (ap h (spglue R r)).
generalize (snd bitot_R b).
apply (Trunc_functor (-1)).
exact (ap h (spglue R r)).
generalize (fst bitot_R a).
apply (Trunc_functor (-1)).
exact (ap H_h (spglue R r)).
generalize (snd bitot_R b).
apply (Trunc_functor (-1)).
exact (ap H_h (spglue R r)).
(** Note that the hypothesis H_setext' differs from the one given in section 10.5 of the HoTT book. *)
Definition V_ind' (P : V -> Type)
(H_0trunc : forall v : V, IsTrunc 0 (P v))
(H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f))
(H_setext' : forall (A B : Type) (f : A -> V) (g : B -> V)
(eq_img: equal_img f g)
(H_f : forall a : A, P (f a)) (H_g : forall b : B, P (g b))
(H_eqimg : (forall a : A, hexists (fun (b : B) =>
hexists (fun (p:f a = g b) => p # (H_f a) = H_g b)))
* (forall b : B, hexists (fun (a : A) =>
hexists (fun (p:f a = g b) => p # (H_f a) = H_g b))) ),
(setext' f g eq_img) # (H_set A f H_f) = (H_set B g H_g)
)
: forall v : V, P v.
apply V_ind with H_set; try assumption.
intros A B R bitot_R h H_h.
pose (f := h o spushl R : A -> V ).
pose (g := h o spushr R : B -> V ).
pose (H_f := H_h oD spushl R : forall a : A, P (f a)).
pose (H_g := H_h oD spushr R : forall b : B, P (g b)).
assert (eq_img : equal_img f g).
generalize (fst bitot_R a).
apply (Trunc_functor (-1)).
exact (ap h (spglue R r)).
generalize (snd bitot_R b).
apply (Trunc_functor (-1)).
exact (ap h (spglue R r)).
transitivity (transport P (setext' (h o spushl R) (h o spushr R) eq_img)
(H_set A (h o spushl R) (H_h oD spushl R))).
apply (ap (fun p => transport P p (H_set A (h o spushl R) (H_h oD spushl R)))).
apply (H_setext' A B f g eq_img H_f H_g).
set (truncb := fst bitot_R a).
apply (Trunc_functor (-1)).
exists (ap h (spglue R Rab)).
apply (concatR (apD H_h (spglue R Rab))).
set (trunca := snd bitot_R b).
apply (Trunc_functor (-1)).
exists (ap h (spglue R Rab)).
apply (concatR (apD H_h (spglue R Rab))).
(** Simpler induction principle when the goal is an hprop *)
Definition V_ind_hprop (P : V -> Type)
(H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f))
(isHProp_P : forall v : V, IsHProp (P v))
: forall v : V, P v.
refine (V_ind _ _ H_set _).
Context `{ua : Univalence}.
(** ** Membership relation *)
Definition mem (x : V) : V -> HProp.
simple refine (V_rec' _ _ _ _).
exact (hexists (fun a : A => f a = x)).
intros A B f g eqimg _ _ _.
apply path_iff_hprop; simpl.
generalize (fst eqimg a).
apply (Trunc_functor (-1)).
transitivity (f a); auto with path_hints.
generalize (snd eqimg b).
apply (Trunc_functor (-1)).
transitivity (g b); auto with path_hints.
Notation "x ∈ v" := (mem x v) : set_scope.
(** ** Subset relation *)
Definition subset (x : V) (y : V) : HProp
:= Build_HProp (forall z : V, z ∈ x -> z ∈ y).
Notation "x ⊆ y" := (subset x y) : set_scope.
(** ** Bisimulation relation *)
(** The equality in V lives in Type@{U'}. We define the bisimulation relation which is a U-small resizing of the equality in V: it must live in HProp_U : Type{U'}, hence the codomain is HProp@{U}. We then prove that bisimulation is equality (bisim_equals_id), then use it to prove the key lemma monic_set_present. *)
(* We define bisimulation by double induction on V. We first fix the first argument as set(A,f) and define bisim_aux : V -> HProp, by induction. This is the inner of the two inductions. *)
Local Definition bisim_aux (A : Type) (f : A -> V) (H_f : A -> V -> HProp) : V -> HProp.
apply V_rec' with
(fun B g _ => Build_HProp ( (forall a, hexists (fun b => H_f a (g b)))
* forall b, hexists (fun a => H_f a (g b)) )
).
intros B B' g g' eq_img H_g H_g' H_img; simpl.
apply path_iff_hprop; simpl.
refine (Trunc_rec _ (H1 a)).
generalize (fst eq_img b).
refine (@Trunc_functor (-1) {b0 : B' & g b = g' b0} {b0 : B' & H_f a (g' b0)} _).
exact (transport (fun x => H_f a x) p H3).
refine (Trunc_rec _ (snd eq_img b')).
apply (Trunc_functor (-1)).
exact (transport (fun x => H_f a x) p H3).
refine (Trunc_rec _ (H1 a)).
generalize (snd eq_img b').
apply (Trunc_functor (-1)).
exact (transport (fun x => H_f a x) p^ H3).
refine (Trunc_rec _ (fst eq_img b)).
apply (Trunc_functor (-1)).
exact (transport (fun x => H_f a x) p^ H3).
(* Then we define bisim : V -> (V -> HProp) by induction again *)
Definition bisimulation : V@{U' U} -> V@{U' U} -> HProp@{U}.
refine (V_rec' (V -> HProp) _ bisim_aux _).
intros A B f g eq_img H_f H_g H_img.
refine (V_ind_hprop _ _ _).
apply path_iff_hprop; simpl.
refine (Trunc_rec _ (snd H_img b)).
apply (Trunc_functor (-1)).
exact ((ap10 p (h c)) # H3).
refine (Trunc_rec _ (H2 c)).
generalize (fst H_img a).
apply (Trunc_functor (-1)).
exact ((ap10 p (h c)) # H3).
refine (Trunc_rec _ (fst H_img a)).
apply (Trunc_functor (-1)).
exact ((ap10 p^ (h c)) # H3).
refine (Trunc_rec _ (H2 c)).
generalize (snd H_img b).
apply (Trunc_functor (-1)).
exact ((ap10 p^ (h c)) # H3).
Notation "u ~~ v" := (bisimulation u v) : set_scope.
Global Instance reflexive_bisimulation : Reflexive bisimulation.
refine (V_ind_hprop _ _ _).
intro a; apply tr; exists a; auto.
intro a; apply tr; exists a; auto.
Lemma bisimulation_equiv_id : forall u v : V, (u = v) <~> (u ~~ v).
intro p; exact (transport (fun x => u ~~ x) p (reflexive_bisimulation u)).
refine (V_ind_hprop _ _ _); intros A f H_f.
refine (V_ind_hprop _ _ _); intros B g _.
apply (Trunc_functor (-1)).
exists b; exact (H_f a (g b) h).
apply (Trunc_functor (-1)).
exists a; exact (H_f a (g b) h).
(** ** Canonical presentation of V-sets (Lemma 10.5.6) *)
(** Using the regular kernel would lead to a universe inconsistency in the monic_set_present lemma later. *)
Definition ker_bisim {A} (f : A -> V) (x y : A) := (f x ~~ f y).
Definition ker_bisim_is_ker {A} (f : A -> V)
: forall (x y : A), f x = f y <~> ker_bisim f x y.
intros; apply bisimulation_equiv_id.
Section MonicSetPresent_Uniqueness.
(** Given u : V, we want to show that the representation u = @set Au mu, where Au is an hSet and mu is monic, is unique. *)
Context {u : V} {Au Au': Type} {h : IsHSet Au} {h' : IsHSet Au'} {mu : Au -> V} {mono : IsEmbedding mu}
{mu' : Au' -> V} {mono' : IsEmbedding mu'} {p : u = set mu} {p' : u = set mu'}.
Lemma eq_img_untrunc : (forall a : Au, {a' : Au' & mu' a' = mu a})
* (forall a' : Au', {a : Au & mu a = mu' a'}).
exact (@untrunc_istrunc (-1) _ (mono' (mu a)) (transport (fun x => mu a ∈ x) (p^ @ p') (tr (a; 1)))).
exact (@untrunc_istrunc (-1) _ (mono (mu' a')) (transport (fun x => mu' a' ∈ x) (p'^ @ p) (tr (a'; 1)))).
Let e : Au -> Au' := fun a => pr1 (fst eq_img_untrunc a).
Let inv_e : Au' -> Au := fun a' => pr1 (snd eq_img_untrunc a').
Let hom1 : e o inv_e == idmap.
apply (isinj_embedding mu' mono').
transitivity (mu (inv_e a')).
exact (pr2 (fst eq_img_untrunc (inv_e a'))).
exact (pr2 (snd eq_img_untrunc a')).
Let hom2 : inv_e o e == idmap.
apply (isinj_embedding mu mono).
transitivity (mu' (e a)).
exact (pr2 (snd eq_img_untrunc (e a))).
exact (pr2 (fst eq_img_untrunc a)).
apply path_universe_uncurried.
apply (equiv_adjointify inv_e e hom2 hom1).
Lemma mu_eq_mu' : transport (fun A : Type => A -> V) path^ mu = mu'.
transitivity (transport (fun X => V) path^ (mu (transport (fun X : Type => X) path^^ a'))).
apply (@transport_arrow Type (fun X : Type => X) (fun X => V) Au Au' path^ mu a').
transitivity (mu (transport idmap path^^ a')).
transitivity (mu (inv_e a')).
2: apply (pr2 (snd eq_img_untrunc a')).
transitivity (transport idmap path a').
exact (ap (fun x => transport idmap x a') (inv_V path)).
apply transport_path_universe.
Lemma monic_set_present_uniqueness : (Au; (mu; (h, mono, p))) = (Au'; (mu'; (h', mono', p'))) :> {A : Type & {m : A -> V & IsHSet A * IsEmbedding m * (u = set m)}}.
apply path_sigma_uncurried; simpl.
transitivity (path^ # mu; transportD (fun A => A -> V) (fun A m => IsHSet A * IsEmbedding m * (u = set m)) path^ mu (h, mono, p)).
apply (@transport_sigma Type (fun A => A -> V) (fun A m => IsHSet A * IsEmbedding m * (u = set m)) Au Au' path^ (mu; (h, mono, p))).
apply path_sigma_hprop; simpl.
End MonicSetPresent_Uniqueness.
(** This lemma actually says a little more than 10.5.6, i.e., that Au is a hSet *)
Lemma monic_set_present : forall u : V, exists (Au : Type) (m : Au -> V),
(IsHSet Au) * (IsEmbedding m) * (u = set m).
destruct (quotient_kernel_factor_general f (ker_bisim f) (ker_bisim_is_ker f))
as [Au [eu [mu (((hset_Au, epi_eu), mono_mu), factor)]]].
split;[exact (hset_Au, mono_mu)|].
intro IC; refine (Trunc_functor (-1) _ (@center _ IC)).
transitivity (mu (eu a)).
intros [Au [mu ((hset, mono), p)]].
intros [Au' [mu' ((hset', mono'), p')]].
apply monic_set_present_uniqueness.
Definition type_of_members (u : V) : Type := pr1 (monic_set_present u).
Notation "[ u ]" := (type_of_members u) : set_scope.
Definition func_of_members {u : V} : [u] -> V := pr1 (pr2 (monic_set_present u)) : [u] -> V.
Definition is_hset_typeofmembers {u : V} : IsHSet ([u]) := fst (fst (pr2 (pr2 (monic_set_present u)))).
Definition IsEmbedding_funcofmembers {u : V} : IsEmbedding func_of_members := snd (fst (pr2 (pr2 (monic_set_present u)))).
Definition is_valid_presentation (u : V) : u = set func_of_members := snd (pr2 (pr2 (monic_set_present u))).
(** ** Lemmas 10.5.8 (i) & (vii), we put them here because they are useful later *)
Lemma extensionality : forall {x y : V}, (x ⊆ y * y ⊆ x) <-> x = y.
refine (V_ind_hprop _ _ _).
refine (V_ind_hprop _ _ _).
refine (Trunc_rec _ (H1 (f a) (tr (a;1)))).
apply tr; exists b; reflexivity.
apply (transport (fun x => z ∈ x) p Hz).
apply (transport (fun x => z ∈ x) p^ Hz).
Lemma mem_induction (C : V -> HProp)
: (forall v, (forall x, x ∈ v -> C x) -> C v) -> forall v, C v.
refine (V_ind_hprop _ _ _).
generalize Hx; apply Trunc_rec.
exact (transport C p (H_f a)).
(** ** Two useful lemmas *)
Global Instance irreflexive_mem : Irreflexive mem.
assert (forall v, IsHProp (complement (fun x x0 : V => x ∈ x0) v v)).
(* https://coq.inria.fr/bugs/show_bug.cgi?id=3854 *)
refine (mem_induction (fun x => Build_HProp (~ x ∈ x)) _); simpl in *.
Lemma path_V_eqimg {A B} {f : A -> V} {g : B -> V} : set f = set g -> equal_img f g.
assert (H : f a ∈ set g).
apply (snd extensionality p).
apply tr; exists a; reflexivity.
generalize H; apply (Trunc_functor (-1)).
assert (H : g b ∈ set f).
apply (snd extensionality p^).
apply tr; exists b; reflexivity.
generalize H; apply (Trunc_functor (-1)).
(** ** Definitions of particular sets in V *)
(** The empty set *)
Definition V_empty : V := set (Empty_ind (fun _ => V)).
Definition V_singleton (u : V) : V@{U' U} := set (Unit_ind u).
Global Instance isequiv_ap_V_singleton {u v : V}
: IsEquiv (@ap _ _ V_singleton u v).
simple refine (Build_IsEquiv _ _ _ _ _ _ _); try solve [ intro; apply path_ishprop ].
specialize (path_V_eqimg H).
refine (Trunc_rec _ (H1 tt)).
Definition V_pair (u : V) (v : V) : V@{U' U} := set (fun b : Bool => if b then u else v).
Lemma path_pair {u v u' v' : V@{U' U}} : (u = u') * (v = v') -> V_pair u v = V_pair u' v'.
apply tr; exists false; assumption.
apply tr; exists true; assumption.
apply tr; exists false; assumption.
Lemma pair_eq_singleton {u v w : V} : V_pair u v = V_singleton w <-> (u = w) * (v = w).
destruct (path_V_eqimg H) as (H1, H2).
refine (Trunc_rec _ (H1 true)).
intros [t p]; destruct t.
refine (Trunc_rec _ (H1 false)).
intros [t p']; destruct t.
split; [exact p| exact p'].
intro a; apply tr; exists tt.
destruct a; [exact p1 | exact p2].
intro t; apply tr; exists true.
(** The ordered pair (u,v) *)
Definition V_pair_ord (u : V) (v : V) : V := V_pair (V_singleton u) (V_pair u v).
Notation " [ u , v ] " := (V_pair_ord u v) : set_scope.
Lemma path_pair_ord {a b c d : V} : [a, b] = [c, d] <-> (a = c) * (b = d).
assert (H : V_singleton a ∈ [c, d]).
apply (snd extensionality p).
apply tr; exists true; reflexivity.
intros [t p']; destruct t.
apply ((ap V_singleton)^-1 p'^).
symmetry; apply (fst pair_eq_singleton p').
assert (H : hor (b = c) (b = d)).
assert (H' : V_pair a b ∈ [c, d]).
apply (snd extensionality p).
apply tr; exists false; reflexivity.
intros [t p']; destruct t.
apply (fst pair_eq_singleton p'^).
destruct (path_V_eqimg p') as (H1, H2).
generalize (H2 false); apply (Trunc_functor (-1)).
intros [t p'']; destruct t.
intro case; destruct case as [p'| p'].
assert (H' : [a, b] = V_singleton (V_singleton b)).
apply (snd pair_eq_singleton).
apply ap; exact (p1 @ p'^).
apply (snd pair_eq_singleton).
split; [exact (p1 @ p'^) | reflexivity].
assert (H'' : V_pair c d = V_singleton b)
by apply (fst pair_eq_singleton (p^ @ H')).
symmetry; apply (fst pair_eq_singleton H'').
split; assumption; assumption.
(** The cartesian product a × b *)
Definition V_cart_prod (a : V) (b : V) : V
:= set (fun x : [a] * [b] => [func_of_members (fst x), func_of_members (snd x)]).
Notation " a × b " := (V_cart_prod a b) : set_scope.
(** f is a function with domain a and codomain b *)
Definition V_is_func (a : V) (b : V) (f : V) := f ⊆ (a × b)
* (forall x, x ∈ a -> hexists (fun y => y ∈ b * [x,y] ∈ f))
* (forall x y y', [x,y] ∈ f * [x,y'] ∈ f -> y = y').
(** The set of functions from a to b *)
Definition V_func (a : V) (b : V) : V
:= @set ([a] -> [b]) (fun f => set (fun x => [func_of_members x, func_of_members (f x)] )).
(** The union of a set Uv *)
Definition V_union (v : V) :=
@set ({x : [v] & [func_of_members x]}) (fun z => func_of_members (pr2 z)).
(** The ordinal successor x ∪ {x} *)
Definition V_succ : V -> V.
simple refine (V_rec' _ _ _ _).
exact (set (fun (x : A + Unit) => match x with inl a => f a
| inr tt => set f end)).
simpl; intros A B f g eq_img _ _ _.
generalize (fst eq_img a).
apply (Trunc_functor (-1)).
apply tr; exists (inr tt).
generalize (snd eq_img b).
apply (Trunc_functor (-1)).
apply tr; exists (inr tt).
(** The set of finite ordinals *)
Definition V_omega : V
:= set (fix I n := match n with 0 => V_empty
| S n => V_succ (I n) end).
(** ** Axioms of set theory (theorem 10.5.8) *)
Lemma not_mem_Vempty : forall x, ~ (x ∈ V_empty).
generalize Hx; apply Trunc_rec.
Lemma pairing : forall u v, hexists (fun w => forall x, x ∈ w <-> hor (x = u) (x = v)).
intro; split; apply (Trunc_functor (-1)).
intros [[|] p]; [left|right]; exact p^.
intros [p | p]; [exists true | exists false]; exact p^.
Lemma infinity : (V_empty ∈ V_omega) * (forall x, x ∈ V_omega -> V_succ x ∈ V_omega).
apply tr; exists 0; auto.
apply (Trunc_functor (-1)).
Lemma union : forall v, hexists (fun w => forall x, x ∈ w <-> hexists (fun u => x ∈ u * u ∈ v)).
apply tr; exists (V_union v).
generalize H; apply (Trunc_functor (-1)).
intros [[u' x'] p]; simpl in p.
exists (func_of_members u'); split.
refine (transport (fun z => x ∈ z) (is_valid_presentation (func_of_members u'))^ _).
refine (transport (fun z => func_of_members u' ∈ z) (is_valid_presentation v)^ _).
apply tr; exists u'; reflexivity.
generalize (transport (fun z => u ∈ z) (is_valid_presentation v) Hu).
generalize (transport (fun z => x ∈ z) (is_valid_presentation (func_of_members u')) (transport (fun z => x ∈ z) pu^ Hx)).
Lemma function : forall u v, hexists (fun w => forall x, x ∈ w <-> V_is_func u v x).
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).
generalize (transport (fun x => z ∈ x) p_phi^ Hz).
apply (Trunc_functor (-1)).
generalize (transport (fun y => x ∈ y) memb_u Hx).
generalize H; apply (Trunc_functor (-1)).
exists (func_of_members (h a)).
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).
generalize H; apply Trunc_rec.
generalize (transport (fun z => [x, y] ∈ z) p_phi^ Hy).
generalize (transport (fun z => [x, y'] ∈ z) p_phi^ Hy').
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 _).
apply (isinj_embedding func_of_members IsEmbedding_funcofmembers a a' (px @ px'^)).
assert (h : forall a : [u], {b : [v] & [func_of_members a, func_of_members b] ∈ phi}).
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))))).
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')).
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].
exact (transport (fun z => [x, z] ∈ phi) Hb^ H2_y).
apply tr; exists (fun a => pr1 (h a)).
generalize Hz; apply Trunc_rec.
exact (transport (fun w => w ∈ phi) Ha (pr2 (h a))).
apply (Trunc_functor (-1)).
transitivity ([func_of_members a, func_of_members b]); auto with path_hints.
apply H3 with (func_of_members a).
exact (transport (fun w => w ∈ phi) p^ Hz).
Lemma replacement : forall (r : V -> V) (x : V),
hexists (fun w => forall y, y ∈ w <-> hexists (fun z => z ∈ x * (r z = y))).
refine (V_ind_hprop _ _ _).
apply (Trunc_functor (-1)).
apply tr; exists a; auto.
apply (Trunc_functor (-1)).
transitivity (r z); auto with path_hints.
Lemma separation (C : V -> HProp) : forall a : V,
hexists (fun w => forall x, x ∈ w <-> x ∈ a * (C x)).
refine (V_ind_hprop _ _ _).
exists (set (fun z : {a : A & C (f a)} => f (pr1 z))).
apply tr; exists a; assumption.
apply (Trunc_functor (-1)).
exists (a; transport C p^ H2).