The cumulative hierarchy V.

Require Import HoTT.Basics HoTT.Basics.Utf8 HoTT.Types.
Require Import HProp HSet TruncType.
Require Import Colimits.SpanPushout.
Require Import HoTT.Truncations Colimits.Quotient.
Local Open Scope nat_scope.
Local Open Scope path_scope.

Bitotal relation

Definition bitotal {A B : Type} (R : A B hProp) :=
( a : A, hexists (fun (b : B) ⇒ R a b))
× ( b : B, hexists (fun (a : A) ⇒ R a b)).

The cumulative hierarchy V

Module Export CumulativeHierarchy.

Private Inductive V : Type@{U'} :=
| set {A : Type@{U}} (f : A V) : V.

Axiom setext : {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 is0trunc_V : IsTrunc 0 V.
Existing Instance is0trunc_V.

Fixpoint V_ind (P : V Type)
(H_0trunc : v : V, IsTrunc 0 (P v))
(H_set : (A : Type) (f : A V) (H_f : a : A, P (f a)), P (set f))
(H_setext : (A B : Type) (R : A B hProp) (bitot_R : bitotal R)
(h : SPushout R V) (H_h : 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) )
(v : V)
: P v
:= (match v with
| set A ffun _ _H_set A f (fun aV_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

End CumulativeHierarchy.

Definition V_comp_setext (P : V Type)
(H_0trunc : v : V, IsTrunc 0 (P v))
(H_set : (A : Type) (f : A V) (H_f : a : A, P (f a)), P (set f))
(H_setext : (A B : Type) (R : A B hProp) (bitot_R : bitotal R)
(h : SPushout R V) (H_h : 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).
Proof.
apply path_ishprop.
Defined.

The non-dependent eliminator

Definition V_rec (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : (A : Type), (A V) (A P) P)
(H_setext : (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.
Proof.
refine (V_ind _ _ H_set _).
intros. exact (transport_const _ _ @ H_setext A B R bitot_R h H_h).
Defined.

Definition V_comp_nd_setext (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : (A : Type), (A V) (A P) P)
(H_setext : (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).
Proof.
apply path_ishprop.
Defined.

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) :=
( a : A, hexists (fun (b : B) ⇒ f a = g b))
× ( 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.
Proof.
pose (R := fun a bBuildhProp (f a = g b)).
pose (h := SPushout_rec R V f g (fun _ _ rr)).
exact (setext R eq_img h).
Defined.

Definition V_rec' (P : Type)
(H_0trunc : IsTrunc 0 P)
(H_set : (A : Type), (A V) (A P) P)
(H_setext' : (A B : Type) (f : A V) (g : B V), (equal_img f g)
(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.
Proof.
refine (V_rec _ _ H_set _).
intros A B R bitot_R h H_h.
apply H_setext'.
- split.
+ intro a. generalize (fst bitot_R a). apply (Trunc_functor (-1)).
intros [b r]. b. exact (ap h (spglue R r)).
+ intro b. generalize (snd bitot_R b). apply (Trunc_functor (-1)).
intros [a r]. a. exact (ap h (spglue R r)).
- split.
+ intro a. generalize (fst bitot_R a). apply (Trunc_functor (-1)).
intros [b r]. b. exact (ap H_h (spglue R r)).
+ intro b. generalize (snd bitot_R b). apply (Trunc_functor (-1)).
intros [a r]. a. exact (ap H_h (spglue R r)).
Defined.

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 : v : V, IsTrunc 0 (P v))
(H_set : (A : Type) (f : A V) (H_f : a : A, P (f a)), P (set f))
(H_setext' : (A B : Type) (f : A V) (g : B V)
(eq_img: equal_img f g)
(H_f : a : A, P (f a)) (H_g : b : B, P (g b))
(H_eqimg : ( a : A, hexists (fun (b : B) ⇒
hexists (fun (p:f a = g b) ⇒ p # (H_f a) = H_g b)))
× ( 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)
)
: v : V, P v.
Proof.
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 : a : A, P (f a)).
pose (H_g := H_h oD spushr R : b : B, P (g b)).
assert (eq_img : equal_img f g).
{ split.
- intro a. generalize (fst bitot_R a). apply (Trunc_functor (-1)).
intros [b r]. b. exact (ap h (spglue R r)).
- intro b. generalize (snd bitot_R b). apply (Trunc_functor (-1)).
intros [a r]. a. 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 ptransport P p (H_set A (h o spushl R) (H_h oD spushl R)))).
apply path_ishprop. }
apply (H_setext' A B f g eq_img H_f H_g). split.
- intro a.
set (truncb := fst bitot_R a). generalize truncb.
apply (Trunc_functor (-1)).
intros [b Rab]. b.
apply tr.
(ap h (spglue R Rab)).
apply (concatR (apD H_h (spglue R Rab))).
apply inverse. unfold f, g. apply transport_compose.
- intros b.
set (trunca := snd bitot_R b). generalize trunca.
apply (Trunc_functor (-1)).
intros [a Rab]. a.
apply tr.
(ap h (spglue R Rab)).
apply (concatR (apD H_h (spglue R Rab))).
apply inverse. unfold f, g. apply transport_compose.
Defined.

Simpler induction principle when the goal is an hprop

Definition V_ind_hprop (P : V Type)
(H_set : (A : Type) (f : A V) (H_f : a : A, P (f a)), P (set f))
(isHProp_P : v : V, IsHProp (P v))
: v : V, P v.
Proof.
refine (V_ind _ _ H_set _).
intros. apply path_ishprop.
Defined.

Section AssumingUA.
Context `{ua : Univalence}.

Membership relation

Definition mem (x : V) : V hProp.
Proof.
simple refine (V_rec' _ _ _ _).
- intros A f _.
exact (hexists (fun a : Af a = x)).
- simpl.
intros A B f g eqimg _ _ _.
apply path_iff_hprop; simpl.
+ intro H. refine (Trunc_rec _ H).
intros [a p]. generalize (fst eqimg a). apply (Trunc_functor (-1)).
intros [b p']. b. transitivity (f a); auto with path_hints.
+ intro H. refine (Trunc_rec _ H).
intros [b p]. generalize (snd eqimg b). apply (Trunc_functor (-1)).
intros [a p']. a. transitivity (g b); auto with path_hints.
Defined.

Declare Scope set_scope.
Notation "x ∈ v" := (mem x v) : set_scope.
Open Scope set_scope.

Subset relation

Definition subset (x : V) (y : V) : hProp
:= BuildhProp ( 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.

Local Definition bisim_aux (A : Type) (f : A V) (H_f : A V hProp) : V hProp.
Proof.
apply V_rec' with
(fun B g _BuildhProp ( ( a, hexists (fun bH_f a (g b)))
× b, hexists (fun aH_f a (g b)) )
).
- exact _.
- intros B B' g g' eq_img H_g H_g' H_img; simpl.
apply path_iff_hprop; simpl.
+ intros [H1 H2]; split.
× intro a. refine (Trunc_rec _ (H1 a)).
intros [b H3]. generalize (fst eq_img b).
unfold hexists. refine (@Trunc_functor (-1) {b0 : B' & g b = g' b0} {b0 : B' & H_f a (g' b0)} _).
intros [b' p]. b'. exact (transport (fun xH_f a x) p H3).
× intro b'. refine (Trunc_rec _ (snd eq_img b')).
intros [b p]. generalize (H2 b). apply (Trunc_functor (-1)).
intros [a H3]. a. exact (transport (fun xH_f a x) p H3).
+ intros [H1 H2]; split.
× intro a. refine (Trunc_rec _ (H1 a)).
intros [b' H3]. generalize (snd eq_img b'). apply (Trunc_functor (-1)).
intros [b p]. b. exact (transport (fun xH_f a x) p^ H3).
× intro b. refine (Trunc_rec _ (fst eq_img b)).
intros [b' p]. generalize (H2 b'). apply (Trunc_functor (-1)).
intros [a H3]. a. exact (transport (fun xH_f a x) p^ H3).
Defined.

Definition bisimulation : V@{U' U} V@{U' U} hProp@{U}.
Proof.
refine (V_rec' (V hProp) _ bisim_aux _).
intros A B f g eq_img H_f H_g H_img.
apply path_forall.
refine (V_ind_hprop _ _ _).
intros C h _; simpl.
apply path_iff_hprop; simpl.
- intros [H1 H2]; split.
+ intro b. refine (Trunc_rec _ (snd H_img b)).
intros [a p]. generalize (H1 a). apply (Trunc_functor (-1)).
intros [c H3]. c. exact ((ap10 p (h c)) # H3).
+ intro c. refine (Trunc_rec _ (H2 c)).
intros [a H3]. generalize (fst H_img a). apply (Trunc_functor (-1)).
intros [b p]. b. exact ((ap10 p (h c)) # H3).
- intros [H1 H2]; split.
+ intro a. refine (Trunc_rec _ (fst H_img a)).
intros [b p]. generalize (H1 b). apply (Trunc_functor (-1)).
intros [c H3]. c. exact ((ap10 p^ (h c)) # H3).
+ intro c. refine (Trunc_rec _ (H2 c)).
intros [b H3]. generalize (snd H_img b). apply (Trunc_functor (-1)).
intros [a p]. a. exact ((ap10 p^ (h c)) # H3).
Defined.

Notation "u ~~ v" := (bisimulation u v) : set_scope.

Global Instance reflexive_bisimulation : Reflexive bisimulation.
Proof.
refine (V_ind_hprop _ _ _).
intros A f H_f; simpl. split.
- intro a; apply tr; a; auto.
- intro a; apply tr; a; auto.
Defined.

Lemma bisimulation_equiv_id : u v : V, (u = v) <~> (u ~~ v).
Proof.
intros u v.
apply equiv_iff_hprop.
- intro p; exact (transport (fun xu ~~ x) p (reflexive_bisimulation u)).
- generalize u v.
refine (V_ind_hprop _ _ _); intros A f H_f.
refine (V_ind_hprop _ _ _); intros B g _.
simpl; intros [H1 H2].
apply setext'. split.
+ intro a. generalize (H1 a). apply (Trunc_functor (-1)).
intros [b h]. b; exact (H_f a (g b) h).
+ intro b. generalize (H2 b). apply (Trunc_functor (-1)).
intros [a h]. a; exact (H_f a (g b) h).
Defined.

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)
: (x y : A), f x = f y <~> ker_bisim f x y.
Proof.
intros; apply bisimulation_equiv_id.
Defined.

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 : ( a : Au, {a' : Au' & mu' a' = mu a})
× ( a' : Au', {a : Au & mu a = mu' a'}).
Proof.
split.
- intro a. exact (@untrunc_istrunc (-1) _ (mono' (mu a)) (transport (fun xmu a x) (p^ @ p') (tr (a; 1)))).
- intro a'. exact (@untrunc_istrunc (-1) _ (mono (mu' a')) (transport (fun xmu' a' x) (p'^ @ p) (tr (a'; 1)))).
Defined.

Let e : Au Au' := fun apr1 (fst eq_img_untrunc a).
Let inv_e : Au' Au := fun a'pr1 (snd eq_img_untrunc a').

Let hom1 : Sect inv_e e.
Proof.
intro a'.
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')).
Defined.

Let hom2 : Sect e inv_e.
Proof.
intro a.
apply (isinj_embedding mu mono).
transitivity (mu' (e a)).
- exact (pr2 (snd eq_img_untrunc (e a))).
- exact (pr2 (fst eq_img_untrunc a)).
Defined.

Let path : Au' = Au.
Proof.
apply path_universe_uncurried.
apply (equiv_adjointify inv_e e hom2 hom1).
Defined.

Lemma mu_eq_mu' : transport (fun A : TypeA V) path^ mu = mu'.
Proof.
apply path_forall. intro a'.
transitivity (transport (fun XV) path^ (mu (transport (fun X : TypeX) path^^ a'))).
- apply (@transport_arrow Type (fun X : TypeX) (fun XV) Au Au' path^ mu a').
- transitivity (mu (transport idmap path^^ a')).
+ apply transport_const.
+ transitivity (mu (inv_e a')).
2: apply (pr2 (snd eq_img_untrunc a')).
refine (ap mu _).
transitivity (transport idmap path a').
× exact (ap (fun xtransport idmap x a') (inv_V path)).
× apply transport_path_universe.
Defined.

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)}}.
Proof.
apply path_sigma_uncurried; simpl.
path^.
transitivity (path^ # mu; transportD (fun AA V) (fun A mIsHSet A × IsEmbedding m × (u = set m)) path^ mu (h, mono, p)).
- apply (@transport_sigma Type (fun AA V) (fun A mIsHSet A × IsEmbedding m × (u = set m)) Au Au' path^ (mu; (h, mono, p))).
- apply path_sigma_hprop; simpl.
exact mu_eq_mu'.
Defined.

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 : u : V, (Au : Type) (m : Au V),
(IsHSet Au) × (IsEmbedding m) × (u = set m).
Proof.
apply V_ind_hprop.
- intros A f _.
destruct (quotient_kernel_factor f (ker_bisim f) (ker_bisim_is_ker f))
as [Au [eu [mu (((hset_Au, epi_eu), mono_mu), factor)]]].
Au, mu. split;[exact (hset_Au, mono_mu)|].
apply setext'; split.
+ intro a. apply tr; (eu a). exact (ap10 factor a).
+ intro a'. generalize (epi_eu a').
intros ?; refine (Trunc_functor (-1) _ (center _)).
intros [a p]. a. transitivity (mu (eu a)).
× exact (ap10 factor a).
× exact (ap mu p).
- intro v. apply hprop_allpath.
intros [Au [mu ((hset, mono), p)]].
intros [Au' [mu' ((hset', mono'), p')]].
apply monic_set_present_uniqueness.
Defined.

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 : {x y : V}, (x y × y x) x = y.
Proof.
refine (V_ind_hprop _ _ _). intros A f _.
refine (V_ind_hprop _ _ _). intros B g _.
split.
- intros [H1 H2]. apply setext'. split.
+ intro. refine (Trunc_rec _ (H1 (f a) (tr (a;1)))).
intros [b p]. apply tr. b. exact p^.
+ intro. apply (H2 (g b)). apply tr; b; reflexivity.
- intro p; split.
+ intros z Hz. apply (transport (fun xz x) p Hz).
+ intros z Hz. apply (transport (fun xz x) p^ Hz).
Qed.

Lemma mem_induction (C : V hProp)
: ( v, ( x, x v C x) C v) v, C v.
Proof.
intro H.
refine (V_ind_hprop _ _ _).
intros A f H_f. apply H. intros x Hx.
generalize Hx; apply Trunc_rec.
intros [a p]. exact (transport C p (H_f a)).
Defined.

Two useful lemmas

Global Instance irreflexive_mem : Irreflexive mem.
Proof.
assert ( v, IsHProp (complement (fun x x0 : Vx x0) v v)).   { intro.
unfold complement.
exact _. }
refine (mem_induction (fun xBuildhProp (¬ x x)) _); simpl in ×.
intros v H. intro Hv.
exact (H v Hv Hv).
Defined.

Lemma path_V_eqimg {A B} {f : A V} {g : B V} : set f = set g equal_img f g.
Proof.
intro p. split.
- intro a.
assert (H : f a set g).
{ apply (snd extensionality p).
apply tr; a; reflexivity. }
generalize H; apply (Trunc_functor (-1)). intros [b p']. b; exact p'^.
- intro b.
assert (H : g b set f).
{ apply (snd extensionality p^).
apply tr; b; reflexivity. }
generalize H; apply (Trunc_functor (-1)). intros [a p']. a; exact p'.
Defined.

Definitions of particular sets in V

The empty set
Definition V_empty : V := set (Empty_ind (fun _V)).

The singleton {u}
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).
Proof.
simple refine (Build_IsEquiv _ _ _ _ _ _ _); try solve [ intro; apply path_ishprop ].
{ intro H. specialize (path_V_eqimg H). intros (H1, H2).
refine (Trunc_rec _ (H1 tt)). intros [t p]. destruct t; exact p. }
Defined.

The pair {u,v}
Definition V_pair (u : V) (v : V) : V@{U' U} := set (fun b : Boolif 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'.
Proof.
intros (H1, H2). apply setext'. split.
+ apply Bool_ind.
× apply tr; true. assumption.
× apply tr; false; assumption.
+ apply Bool_ind.
× apply tr; true; assumption.
× apply tr; false; assumption.
Defined.

Lemma pair_eq_singleton {u v w : V} : V_pair u v = V_singleton w (u = w) × (v = w).
Proof.
split.
+ intro H. 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'].
+ intros (p1, p2). apply setext'; split.
× intro a; apply tr; tt. destruct a; [exact p1 | exact p2].
× intro t; apply tr; true. destruct t; exact p1.
Defined.

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).
Proof.
split.
- intro p. assert (p1 : a = c).
+ assert (H : V_singleton a [c, d]).
{ apply (snd extensionality p). simpl.
apply tr; true; reflexivity. }
refine (Trunc_rec _ H). intros [t p']; destruct t.
× apply ((ap V_singleton)^-1 p'^).
× symmetry; apply (fst pair_eq_singleton p').
+ split.
× exact p1.
× assert (H : hor (b = c) (b = d)).
{ assert (H' : V_pair a b [c, d]).
{ apply (snd extensionality p).
apply tr; false; reflexivity. }
refine (Trunc_rec _ H'). intros [t p']; destruct t.
- apply tr; left. 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.
+ left; exact p''^.
+ right; exact p''^. }
refine (Trunc_rec _ H). intro case; destruct case as [p'| p'].
2: assumption.
assert (H' : [a, b] = V_singleton (V_singleton b)).
{ apply (snd pair_eq_singleton).
split.
- 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'').
- intros (p, p').
apply path_pair. split.
+ apply ap; exact p.
+ apply path_pair. split; assumption; assumption.
Defined.

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)
× ( x, x a hexists (fun yy b × [x,y] f))
× ( 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 fset (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 zfunc_of_members (pr2 z)).

The ordinal successor x ∪ {x}
Definition V_succ : V V.
Proof.
simple refine (V_rec' _ _ _ _).
- intros A f _.
exact (set (fun (x : A + Unit) ⇒ match x with inl af a
| inr ttset f end)).
- simpl; intros A B f g eq_img _ _ _. apply setext'. split.
+ intro. destruct a.
× generalize (fst eq_img a). apply (Trunc_functor (-1)).
intros [b p]. (inl b); exact p.
× apply tr; (inr tt). destruct u. apply setext'; auto.
+ intro. destruct b.
× generalize (snd eq_img b). apply (Trunc_functor (-1)).
intros [a p]. (inl a); exact p.
× apply tr; (inr tt). destruct u. apply setext'; auto.
Defined.

The set of finite ordinals
Definition V_omega : V
:= set (fix I n := match n with 0 ⇒ V_empty
| S nV_succ (I n) end).

Axioms of set theory (theorem 10.5.8)

Lemma not_mem_Vempty : x, ¬ (x V_empty).
Proof.
intros x Hx. generalize Hx; apply Trunc_rec.
intros [ff _]. exact ff.
Qed.

Lemma pairing : u v, hexists (fun w x, x w hor (x = u) (x = v)).
Proof.
intros u v. apply tr. (V_pair u v).
intro; split; apply (Trunc_functor (-1)).
- intros [[|] p]; [left|right]; exact p^.
- intros [p | p]; [ true | false]; exact p^.
Qed.

Lemma infinity : (V_empty V_omega) × ( x, x V_omega V_succ x V_omega).
Proof.
split.
- apply tr; 0; auto.
- intro. apply (Trunc_functor (-1)).
intros [n p]. (S n). rewrite p; auto.
Qed.

Lemma union : v, hexists (fun w x, x w hexists (fun ux u × u v)).
Proof.
intro v. apply tr; (V_union v).
intro x; split.
- intro H. simpl in H. generalize H; apply (Trunc_functor (-1)).
intros [[u' x'] p]; simpl in p.
(func_of_members u'); split.
+ refine (transport (fun zx z) (is_valid_presentation (func_of_members u'))^ _).
simpl. apply tr; x'. exact p.
+ refine (transport (fun zfunc_of_members u' z) (is_valid_presentation v)^ _).
simpl. apply tr; u'; reflexivity.
- apply Trunc_rec. intros [u (Hx, Hu)].
generalize (transport (fun zu z) (is_valid_presentation v) Hu).
apply Trunc_rec. intros [u' pu].
generalize (transport (fun zx z) (is_valid_presentation (func_of_members u')) (transport (fun zx z) pu^ Hx)).
apply Trunc_rec. intros [x' px].
apply tr. (u'; x'). exact px.
Qed.

Lemma function : u v, hexists (fun w x, x w V_is_func u v x).
Proof.
intros u v. apply tr; (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 xz x) p_phi^ Hz). apply (Trunc_functor (-1)).
intros [a p]. (a, h a). assumption.
+ intros x Hx. generalize (transport (fun yx y) memb_u Hx).
apply Trunc_rec. intros [a p]. generalize H; apply (Trunc_functor (-1)).
intros [h p_phi]. (func_of_members (h a)). split.
× exact (transport (fun zfunc_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; 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 : 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 zx 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.
(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 zy z) memb_v H1_y)) as [b Hb].
b. exact (transport (fun z[x, z] phi) Hb^ H2_y). }
apply tr; (fun apr1 (h a)). apply extensionality. split.
+ intros z Hz. generalize Hz; apply Trunc_rec. intros [a Ha].
exact (transport (fun ww phi) Ha (pr2 (h a))).
+ intros z Hz. simpl.
generalize (H1 z Hz). apply (Trunc_functor (-1)). intros [(a,b) p]. simpl in p.
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 ww phi) p^ Hz).
Qed.

Lemma replacement : (r : V V) (x : V),
hexists (fun w y, y w hexists (fun zz x × (r z = y))).
Proof.
intro r. refine (V_ind_hprop _ _ _).
intros A f _. apply tr. (set (r o f)). split.
- apply (Trunc_functor (-1)).
intros [a p]. (f a). split.
+ apply tr; a; auto.
+ assumption.
- apply Trunc_rec.
intros [z [h p]]. generalize h. apply (Trunc_functor (-1)).
intros [a p']. a. transitivity (r z); auto with path_hints. exact (ap r p').
Qed.

Lemma separation (C : V hProp) : a : V,
hexists (fun w x, x w x a × (C x)).
Proof.
refine (V_ind_hprop _ _ _).
intros A f _. apply tr. (set (fun z : {a : A & C (f a)}f (pr1 z))). split.
- apply Trunc_rec.
intros [[a h] p]. split. + apply tr; a; assumption. + exact (transport C p h).
- intros [H1 H2]. generalize H1. apply (Trunc_functor (-1)).
intros [a p]. (a; transport C p^ H2). exact p.
Qed.

End AssumingUA.