(* CZF with urelements as described in the paper "Constructing categories and setoids of setoids in type theory" by Erik Palmgren and Olov Wilander 2013. Author: Olov Wilander 2012. Written in Coq 8.3pl2/Coq 8.3pl3 with UTF8-encoding. *) Require Import PropasTypesUtf8Notation PropasTypesBasics_mod SwedishSetoids_mod. Delimit Scope czfu_scope with czfu. Open Scope czfu_scope. Section CZFU. (* The setoid of atoms *) Variable Atom: setoid. (* The type of well-founded trees, that is the universe of CZF sets in the constructed model.*) Inductive V: Type := sup (A: Set) (f: A → V) | atm (a: Atom). Definition set_b (x: V): bool := match x with | sup _ _ => true | atm _ => false end. (* Adding Set-valued predicates for sup and atm in V /EP 2012-06-23 *) Definition isset (x: V): Set := match x with | sup _ _ => ⊤ | atm _ => ⊥ end. Definition isatom (x: V): Set := match x with | sup _ _ => ⊥ | atm _ => ⊤ end. Notation "'set' x" := (isset x) (at level 39) : czfu_scope. Notation "'atom' x" := (isatom x) (at level 39) : czfu_scope. Definition iV (s: V): Set := match s with sup A f => A | atm _ => False end. Coercion iV : V >-> Sortclass. Definition pV (s: V): s → V := match s with sup A f => f | atm _ => (λ x, match x with end) end. Coercion pV : V >-> Funclass. (* The equality relation is the least bisimulation on V *) Fixpoint eqV (x y: V): Set := let Bisim := (λ S T: Set, λ R: S → T → Set, (∀x: S, ∃y: T, R x y) ∧ (∀y: T, ∃x: S, R x y)) in match x with | sup ix fx => match y with | sup iy fy => Bisim ix iy (λ α β, eqV (fx α) (fy β)) | atm ay => False end | atm ax => match y with | sup iy fy => False | atm ay => ax ≈ ay end end. Infix "≐" := eqV (at level 70, no associativity) : czfu_scope. (* Some sanity check lemmas *) Lemma atom_eq: ∀a b: Atom, (a ≈ b) ↔ (atm a ≐ atm b). Proof. auto. Qed. (* The first thing to do is to prove that this is an equivalence relation. *) Theorem refV: ∀x, x ≐ x. Proof. intro x; induction x; [| apply setoidrefl]. split; [intro x; exists x; trivial ..]. Qed. Theorem symV: ∀x y, x ≐ y → y ≐ x. Proof. intro x; induction x as [ix fx IH | ax]. intros [iy fy | ay]. (* !! This needs a tactic *) intros [P0 P1]; fold eqV in P0, P1. split. intro yidx. destruct P1 with yidx as [xidx]. exists xidx. auto. intro xidx. destruct P0 with xidx as [yidx]. exists yidx. auto. auto. intro y; destruct y as [iy fy | ay]. auto. apply setoidsym. Qed. Theorem traV: ∀x y z, x ≐ y → y ≐ z → x ≐ z. Proof. intros x; induction x as [ix fx IH | ax]. intros [iy fy | ay] [iz fz | az]; [| contradiction..]. intros [P0 P1] [Q0 Q1]; fold eqV in P0, P1, Q0, Q1. split. intro xidx; destruct P0 with xidx as [yidx xyeq]; destruct Q0 with yidx as [zidx yzeq]. exists zidx. apply IH with (fy yidx); assumption. intro zidx; destruct Q1 with zidx as [yidx zyeq]; destruct P1 with yidx as [xidx yxeq]. exists xidx. apply IH with (fy yidx); assumption. intros [iy fy | ay] [iz fz | az]; [contradiction.. | apply setoidtra]. Qed. (* Next, define the membership relation... *) Definition memV (x y: V): Set := ∃idx: y, x ≐ y idx. Infix "∈" := memV (at level 70, no associativity) : czfu_scope. Notation "x ∉ y" := (¬(x ∈ y)) (at level 70) : czfu_scope. (* ... and prove that it respects the equality relation introduced earlier. *) Lemma ext1: ∀x y z, x ≐ y → y ∈ z → x ∈ z. Proof. intros x y z H [idx eq]. exists idx. apply traV with y; assumption. Qed. Lemma ext2: ∀x y z, x ∈ y → y ≐ z → x ∈ z. Proof. intros x [iy fy | ay] [iz fz | az]; [| intros []; contradiction..]. intros [idx eq] [P0 P1]; fold eqV in P0, P1. destruct P0 with idx as [idx' eq']. exists idx'. apply traV with (fy idx); assumption. Qed. (* Introduce some more notation *) Notation "x ⊆ y" := (∀z: V, z ∈ x → z ∈ y) (at level 60) : czfu_scope. (* To state the axioms, we will also need the set quantifiers *) Definition Setall (P: V → Type): Type := ∀x: V, set x → P x. Notation "∀ˢ x , P" := (Setall (fun x: V => P)) (at level 100, x ident). Definition Setex (P: V → Type): Type := ∃x: V, set x ∧ P x. Notation "∃ˢ x , P" := (Setex (fun x: V => P)) (at level 100, x ident). (* !! There probably should be tactics for these *) Ltac setexists x := exists x; split; [auto |]. (* Now start proving that the axioms hold *) (* New proof fitting new def. /EP 20120623 *) Theorem SetDecidable: ∀x, set x ∨ atom x. Proof. intro x; destruct x. left. apply tt. right. apply tt. Qed. Theorem AtomsEmpty: ∀x y, atom y → x ∉ y. Proof. intros x [y | a]; [auto|]. intros _ [[]]. Qed. Lemma ext3: ∀ˢx, ∀ˢy, x ⊆ y → y ⊆ x → x ≐ y. Proof. intros [ix fx | ax] xs [iy fy | ay] ys. intros xsuby ysubx; split. intro xidx. destruct xsuby with (fx xidx) as [idx]. exists xidx; apply refV. exists idx; assumption. intro yidx. destruct ysubx with (fy yidx) as [idx]. exists yidx; apply refV. exists idx. apply symV; assumption. elim ys. elim xs. elim xs. Qed. Theorem Extensionality: ∀ˢx, ∀ˢy, (∀z, z ∈ x ↔ z ∈ y) → x ≐ y. Proof. intros x xs y ys H. apply ext3; try (intro z; apply (H z)); assumption. Qed. Definition pairV (x y: V): V := sup bool (λ b, match b with true => x | false => y end). Notation "{{ x , y }}" := (pairV x y) (at level 0, x, y at level 69) : czfu_scope. Lemma pairVL1: ∀x y, x ∈ {{ x, y }}. Proof. intros; exists true; apply refV. Qed. Lemma pairVL2: ∀x y, y ∈ {{ x, y }}. Proof. intros; exists false; apply refV. Qed. Lemma pairingchar: ∀a b y, y ∈ {{ a,b }} ↔ y ≐ a ∨ y ≐ b. Proof. intros a b y; split. intro H; destruct H as [i eq]; simpl in i. destruct i ; [left | right]; [assumption..]. intro H; destruct H as [eq | eq]. apply ext1 with a, pairVL1; assumption. apply ext1 with b, pairVL2; assumption. Qed. Theorem Pairing: ∀a b, ∃ˢc, ∀y, y ∈ c ↔ y ≐ a ∨ y ≐ b. Proof. intros; setexists {{ a, b }}. apply tt. apply pairingchar. Qed. Lemma pairingcharR: ∀a b y, y ∈ {{ a, b }} → y ≐ a ∨ y ≐ b. Proof. intros a b y; eapply pairingchar. Qed. Lemma pairingcharL: ∀a b y, y ≐ a ∨ y ≐ b → y ∈ {{ a, b }}. Proof. intros a b y; eapply pairingchar. Qed. Definition unionV (x: V): V := sup (∃a: x, x a) (λ u, x (projT1 u) (projT2 u)). Notation "⋃ X" := (unionV X) (at level 1) : czfu_scope. Lemma unionLm: ∀s: V, ∀x: s, s x ∈ s. Proof. intros s x; exists x; apply refV. Qed. Lemma unionLm1: ∀s: V, ∀A: Set, ∀f: A → V, ∀x: A, s ∈ f x → s ∈ ⋃(sup A f). Proof. intros s A f x [i eq]. exists (existT _ x i); assumption. Qed. Lemma unionLm2: ∀r s t, r ∈ s → s ∈ t → r ∈ ⋃t. Proof. intros r s [it ft | a'] rs [idx eq]. apply unionLm1 with idx, ext2 with s; [assumption..]. destruct s as [i f | a]; contradiction. Qed. Lemma unionchar: ∀a y, y ∈ ⋃a ↔ ∃x, x ∈ a ∧ y ∈ x. Proof. intros a y; split. intros [[i i'] eq]. simpl in eq. exists (a i); split. apply unionLm. apply ext1 with (a i i'), unionLm; assumption. intro H; destruct H as (x, (xina, yinx)). apply unionLm2 with x; [assumption..]. Qed. Theorem Union: ∀a, ∃ˢb, ∀y, y∈b ↔ ∃x, x ∈ a ∧ y ∈ x. Proof. intro a; setexists ⋃a. apply tt. apply unionchar. Qed. Notation "s ∪ t" := (⋃{{ s, t }}) (at level 65, right associativity) : czfu_scope. Theorem binunionchar: ∀x s t, x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t. Proof. intros x s t; split. intros [[i i'] eq]. destruct i; [left | right]; [ exists i'; assumption ..]. intros [[i eq] | [i eq]]. exists (existT _ true i); assumption. exists (existT _ false i); assumption. Qed. Definition emptyV : V := sup False (False_rect V). Notation "∅" := emptyV : czfu_scope. Theorem EmptySet: ∀x, x ∉ ∅. Proof. intros _ [[]]. Qed. Theorem EmptySetAxiom: ∃ˢx, ∀y, y ∉ x. Proof. setexists ∅. apply tt. apply EmptySet. Qed. Definition extensionalV (P: V → Type): Type := ∀x y, P x → x ≐ y → P y. Notation "« P »" := (extensionalV P) : czfu_scope. Theorem SetInduction (P: V → Type) (Pext: «P»): (∀x, (∀y, y∈x → P y) → P x) → ∀x, P x. Proof. intros IH; induction x as [I f IH' | a]; apply IH. intros y (i, eq). apply symV in eq. apply (Pext (f i) y), eq. apply IH'. intros _ [[]]. Qed. Definition singletonV (x: V) := sup ⊤ (λ _, x). Notation "{{ s }}" := (singletonV s) (at level 0, s at level 69). (* Sanity check lemma for this notation *) Lemma singleton_equals_pair (x: V): {{ x }} ≐ {{ x, x }}. Proof. split. exists true; apply refV. induction y; repeat progress split; apply refV. Qed. Lemma singleton_char (x y: V): x ∈ {{ y }} → x ≐ y. Proof. intros [idx eq]; destruct idx; assumption. Qed. Notation "s ⁺" := (s ∪ {{ s }}) (at level 1) : czfu_scope. Lemma succL1: ∀s t:V, s ∈ t⁺ → s ≐ t ∨ s ∈ t. Proof. intros s t H; destruct (binunionchar s t {{ t }}) as (K, _). apply K in H; clear K; destruct H as [st | stt]. right; assumption. left; apply singleton_char; assumption. Qed. Lemma succL2: ∀s t:V, s ≐ t ∨ s ∈ t → s ∈ t⁺. Proof. intros s t H; destruct H as [sist | sint]. exists (existT _ false tt); assumption. eapply binunionchar; left; assumption. Qed. Fixpoint numeralV (n: ℕ): V := match n with | O => ∅ | S m => (numeralV m)⁺ end. Notation "⌜ n ⌝" := (numeralV n). Definition natV: V := sup ℕ numeralV. Notation ω := natV. Notation ttve x := (∀y z, z ∈ y → y ∈ x → z ∈ x). Theorem numeralsaretransitive: ∀n: ℕ, ttve(⌜n⌝). Proof. induction n. intros y z ziny (i, eq); elim i. intros y z ziny yinSn; apply succL2; apply succL1 in yinSn; fold numeralV in *. destruct yinSn as [yisn | yinn]. right; apply ext2 with y; assumption. right; apply IHn with y; [assumption..]. Qed. Lemma eltnat: ∀n: ℕ, ∀x, x ∈ ⌜n⌝ → ∃m: ℕ, x ≐ ⌜m⌝. Proof. induction n. intros _ [[]]. intros x xinSn; destruct (succL1 x (numeralV n)); [ | exists n | apply IHn]; [assumption..]. Qed. Lemma omegattve: ttve(ω). Proof. intros z y yinz (n, eq). apply (eltnat n), ext2 with z; assumption. Qed. Lemma succext_helper: ∀x y, x ≐ y → x⁺ ⊆ y⁺. Proof. intros x y eq. (* [| apply symV in eq]; *) match goal with |- ?a ⁺ ⊆ ?b ⁺ => (intros r rina; apply binunionchar in rina; apply binunionchar; destruct rina as [rina | risa]; [left; apply ext2 with a; assumption | apply singleton_char in risa; right; exists tt; apply traV with a; assumption ]) end. Qed. Lemma succext: ∀x y, x ≐ y → x⁺ ≐ y⁺. Proof. intros x y eq. apply ext3. apply tt. apply tt. apply succext_helper. assumption. apply succext_helper. apply symV. assumption. Qed. Theorem Infinity: ∃ˢx, ∅ ∈ x ∧ ∀y, y ∈ x → y⁺ ∈ x. Proof. setexists ω; split. exists O; apply refV. intros y (i, eq); exists (S i). apply traV with ((ω i)⁺), refV. apply succext; assumption. Qed. Definition sepV (s: V) (P: V → Set) := sup (∃a: s, P (s a)) (λ u, s (projT1 u)). Notation "{{ x ∈ s | P }}" := (sepV s (fun x => P)) (at level 0, x, s, P at level 69) : czfu_scope. Lemma separationchar (P: V → Set) (Pext: «P»): ∀s x, x ∈ {{ y ∈ s | P y }} ↔ x ∈ s ∧ P x. Proof. intros s x; split. intros ((i, pf), eq); simpl in eq; split. exists i; assumption. apply (Pext (s i)), symV; [assumption..]. intros ((i, eq), pf). apply (Pext x (s i)) in pf; [ | apply eq]. exists (existT (fun u => P (s u)) i pf); assumption. Qed. Theorem Separation (P: V → Set) (Pext: «P»): ∀s, ∃ˢt, ∀x, x∈t ↔ x ∈ s ∧ P x. Proof. intros; setexists ({{ x ∈ s | P x }}). apply tt. apply separationchar; assumption. Qed. Lemma sep_sub (P: V → Set) (Pext: «P»): ∀x, {{ y ∈ x | P y }} ⊆ x. Proof. intros x z [[idx pf] eq]. exists idx; assumption. Qed. (* Definition Ball (s: V) (P: V → Set): Set := ∀x:s, P (s x). Notation "∀ x ∈ s , P" := (Ball s (fun x: V => P)) (at level 200, x at level 0). *) Notation "∀ x ∈ s , P" := (∀x: iV s, (fun x: V => P) (pV s x)) (at level 200, x at level 0). (* Definition Bex (s: V) (P: V → Set): Set := ∃x:s, P (s x). Notation "∃ x ∈ s , P" := (Bex s (fun x: V => P)) (at level 200, x at level 0). *) Notation "∃ x ∈ s , P" := (∃x: iV s, (fun x: V => P) (pV s x)) (at level 200, x at level 0). Lemma Ballright: ∀a, ∀P: V → Set, «P» → ((∀x ∈ a, P x) ↔ ∀x, x ∈ a → P x). Proof. intros a P E; split. intros bdd x (i, eq). apply E with (a i), symV, eq; apply bdd. intros full i; apply full, unionLm. Qed. Lemma Bexright: ∀a, ∀P: V → Set, «P» → ((∃x ∈ a, P x) ↔ ∃x: V, x ∈ a ∧ P x). Proof. intros a P E; split. intros (i, pf); exists (a i); split; [apply unionLm | assumption]. intros (x, ((i, eq), pf)). exists i. apply E with x; [assumption..]. Qed. Lemma SetInductionBdd (P: V → Set) (Pext: «P»): (∀x, (∀y ∈ x, P y) → P x) → ∀x, P x. Proof. intros IH x. induction x as [ix fx IH' | ax]. apply IH. intros idx. apply IH'. apply IH. intros []. Qed. Notation totalV a b R := (∀x ∈ a, ∃y ∈ b, R x y). Notation bitotalV a b R := ((totalV a b R) ∧ (totalV b a (λ x y, R y x))). Theorem StrongCollection: ∀R: V → V → Type, (∀x: V, «λ y, R x y» ∧ «λ y, R y x») → ∀a, (∀x ∈ a, ∃y, R x y) → ∃ˢb, bitotalV a b R. Proof. intros R _ a bdd. destruct (TTAC a V _ bdd) as (f, pf). (* !! Are library choice axioms enough? *) setexists (sup a f); split; [(intro y; exists y; apply pf)..]. Qed. Definition sscV (a b: V): V := (sup (a → b) (λ f, sup a (λ x, b (f x)))). Theorem SubsetCollection: ∀Q: V → V → V → Type, (∀a b: V, «Q a b» ∧ «λ y, Q a y b» ∧ «λ y, Q y a b») → ∀a b, ∃ˢc, ∀u, ((∀x ∈ a, ∃y ∈ b, Q x y u) → ∃d ∈ c, ((∀x ∈ a, ∃y ∈ d, Q x y u) ∧ (∀y ∈ d, ∃x ∈ a, Q x y u))). Proof. intros Q _ a b. setexists (sscV a b). apply tt. intros u abbdd. destruct (TTAC a b _ abbdd) as (f, pf). exists f; split; [(intro x; exists x; apply pf)..]. Qed. (* As it is was assumed that Atom:Setoid, the atoms of the model form a set. /EP *) Definition setofatomsV : V := sup Atom atm. Theorem AtomsFormASet: ∃ˢx, ∀z, z ∈ x ↔ atom z. Proof. setexists setofatomsV. apply tt. intro z. split. intro. destruct z. elim H. intros x p. elim p. apply tt. trivial. intro. destruct z. destruct H. exists a. apply refV. Qed. (* Now start developing basic mathematics inside the model *) Notation "〈 x , y 〉" := ({{ {{ x }}, {{ x, y }} }}). Lemma pairing_injective (x y z w: V): 〈x, z〉 ≐ 〈y, w〉 → x ≐ y ∧ z ≐ w. Proof. intros [eq1 eq2]; fold eqV in *. Time repeat match goal with [hyp: ∀_: bool, _ |- _] => destruct (hyp true); destruct (hyp false); clear hyp end; repeat match goal with [hyp: bool |- _] => destruct hyp end; repeat match goal with [hyp: ?a ≐ ?b, hyp0: ?a ≐ ?b |- _] => clear hyp end; repeat match goal with [hyp: {{ _ }} ≐ {{ _ }} |- _] => let P := fresh in destruct hyp as [P _]; fold eqV in P; destruct (P tt); clear P end; repeat match goal with [hyp: {{ ?a, ?b }} ≐ {{ ?c, ?d }} |- _] => let e1 := fresh in let e2 := fresh in destruct hyp as [e1 e2]; destruct (e1 true); destruct (e1 false); destruct (e2 true); destruct (e2 false); clear e1 e2; fold eqV in * end; repeat match goal with [hyp: bool |- _] => destruct hyp end; repeat match goal with [hyp: ?a ≐ ?b, hyp0: ?a ≐ ?b |- _] => clear hyp end; repeat match goal with [hyp: {{ _, _ }} ≐ {{ _ }} |- _] => apply symV in hyp end; repeat match goal with [hyp: {{ ?a }} ≐ {{ ?b, ?c }} |- _] => let eq1 := fresh in destruct hyp as [_ eq1]; fold eqV in eq1; destruct (eq1 true); destruct (eq1 false); clear eq1 end; repeat match goal with [hyp: ⊤ |- _] => clear hyp end; repeat match goal with [hyp: ?a ≐ ?b, hyp0: ?a ≐ ?b |- _] => clear hyp end; eauto using symV, traV. (* Slower proof: Time repeat match goal with [hyp: ∀α: bool, ∃β: bool, ?P |- _] => let a := fresh in let ap := fresh in destruct (hyp true) as [a ap]; destruct a; destruct ap; destruct (hyp false) as [a ap]; destruct a; destruct ap; fold eqV in *; clear hyp end; repeat match goal with [hyp:(⊤ → ?P) |- _] => assert P; [exact (hyp tt)|]; clear hyp end; repeat match goal with [hyp: ∀_: bool, _ |- _] => destruct (hyp true); destruct (hyp false); clear hyp end; repeat match goal with [hyp: sigT _ |- _] => destruct hyp end; repeat match goal with [hyp: ⊤ |- _] => clear hyp end; repeat match goal with [hyp: bool |- _] => destruct hyp end; repeat match goal with [hyp: ?a ≐ ?b, hyp0: ?a ≐ ?b |- _] => clear hyp end; eauto using symV, traV. *) Qed. Lemma pairing_extensional (x y z w: V): x ≐ z → y ≐ w → 〈x, y〉 ≐ 〈z, w〉. Proof. intros xeqz yeqw. split; intro a; exists a. destruct a. repeat split; assumption. split; intro a; exists a; destruct a; assumption. destruct a. repeat split; assumption. split; intro a; exists a; destruct a; assumption. Qed. Definition prodV (x y: V): V := sup (x ∧ y) (fun p => let (α, β) := p in 〈x α, y β〉). Notation "x × y" := (prodV x y) (at level 40). Lemma productchar (x y: V): ∀z, z ∈ x × y ↔ ∃α ∈ x, ∃β ∈ y, z ≐ 〈α, β〉. Proof. intro z; split. intros [[α β] eq]; simpl in eq. exists α. exists β. assumption. intros [α [β eq]]; exists (α, β); assumption. Qed. Lemma productchar_altproof (x y: V): ∀z, z ∈ x × y ↔ ∃α ∈ x, ∃β ∈ y, z ≐ 〈α, β〉. proof. let z:V. focus on (z ∈ x × y → ∃α ∈ x, ∃β ∈ y, z ≐ 〈α, β〉). given index such that eq: (z ≐ (x × y) index). claim (z ≐ (x × y) index → ∃α ∈ x, ∃β ∈ y, z ≐ 〈α, β〉). consider ix: x, iy: y from index. assume (z ≐ (x × y) (ix, iy)). take ix. take iy. hence thesis. end claim. hence thesis by eq. end focus. given α, β such that (z ≐ 〈x α, y β〉). take (α, β). hence thesis. end proof. Qed. Theorem Products: ∀x y, ∃ˢz, ∀w, w ∈ z ↔ ∃α ∈ x, ∃β ∈ y, w ≐ 〈α, β〉. Proof. intros x y. setexists (x × y). apply tt. apply productchar. Qed. Definition is_rel (x y: V) (R: V): Type := set R ∧ R ⊆ x × y. Definition is_total (x y: V) (R: V): Type := ∀α ∈ x, ∃β ∈ y, 〈α,β〉 ∈ R. Definition is_onto (x y: V) (R: V): Type := ∀β ∈ y, ∃α ∈ x, 〈α,β〉 ∈ R. Definition is_functional (R: V): Type := ∀x y y', 〈x, y〉 ∈ R ∧ 〈x, y'〉 ∈ R → y ≐ y'. Definition is_function (x y: V) (F: V): Type := is_rel x y F ∧ is_total x y F ∧ is_functional F. Definition identity (x: V): V := {{ p ∈ x × x | ∃y ∈ x, p ≐ 〈y, y〉 }}. Lemma id_is_function {x: V}: is_function x x (identity x). Proof. split. split. apply tt. auto. intros α [[[αi11 αi12] αi2] eq]. exists (αi11, αi12). assumption. split. intro α. exists α. unfold identity. unfold sepV. apply (sigrejig (x ∧ x)). exists (α, α). apply (sigrejig x). exists α. exists (refV 〈x α, x α〉). simpl. split; intro y; exists y; auto using refV. intros y z z' [[yzi yzeq] [yz'i yz'eq]]. repeat match goal with [hyp: (〈y, ?a〉 ≐ (?b ?c)) |- _] => let i := fresh in let j := fresh in let r := fresh in let s := fresh in let t := fresh in destruct c as [[i j] r]; change ((x × x) (i, j)) with (〈x i, x j〉) in r; destruct r as [s t]; change ((identity x) (existT _ (i, j) _)) with (〈x i, x j〉) in hyp end. repeat match goal with [hyp: 〈_, _〉 ≐ 〈_, _〉 |- _] => apply pairing_injective in hyp; destruct hyp end. apply traV with y; eauto using symV, traV. Qed. Definition functionspace (x y:V): V := sup (∃f:x→y, ∀α β:x, x α ≐ x β → y (f α) ≐ y (f β)) (fun p => match p with existT f _ => sup x (fun α => 〈x α, y (f α)〉) end). (* Triple arrow UTF-8 functionspaces in V /EP *) Notation "A ⇛ B" := (functionspace A B) (at level 55, right associativity). Lemma functionspacechar (x y: V) : ∀z, z ∈ x ⇛ y ↔ is_function x y z. Proof. intros [iz fz | az]; split. intros [[f pf] [eq1 eq2]]; fold eqV in eq1, eq2. split. split. auto. apply tt. intros α [iα eqα]. clear eq2. simpl in iα, eqα. specialize eq1 with iα. destruct eq1 as [idx idxeq]. exists (idx, f idx). eauto using symV, traV. split; intro α. specialize eq2 with α. destruct eq2 as [γ γeq]. exists (f α). exists γ. apply symV; assumption. intros β β' [[iγ eqγ] [iγ' eqγ']]. simpl in iγ, iγ'. destruct (eq1 iγ) as [xγ eqxγ]. apply (traV 〈α, β〉) in eqxγ; try assumption. apply pairing_injective in eqxγ. specialize eq1 with iγ'. destruct eq1 as [xγ' eqxγ']. apply (traV 〈α, β'〉) in eqxγ'; try assumption. apply pairing_injective in eqxγ'. apply traV with (y (f xγ)). apply eqxγ. apply traV with (y (f xγ')); [| apply symV; apply eqxγ']. apply pf. apply traV with α; [apply symV|]. apply eqxγ. apply eqxγ'. intros [relz [totz funz]]. unfold is_total in totz. apply TTAC in totz. destruct totz as [f fprop]. unfold memV. unfold functionspace. apply (sigrejig (x → y)). exists f. simpl. split. intros α β αeqβ. apply funz with (x α). split. apply fprop. apply ext1 with (〈x β, y (f β)〉). apply pairing_extensional. assumption. apply refV. apply fprop. unfold is_rel in relz. split. intro z. destruct (snd relz) with (fz z) as [[idx1 idx2] eq]. exists z; apply refV. simpl in eq. exists idx1. specialize fprop with idx1. eapply traV; [apply eq|]. apply pairing_extensional. apply refV. apply funz with (x idx1). split. exists z. apply symV; assumption. apply fprop. intro α. specialize fprop with α. destruct fprop as [idx eq]. exists idx. apply symV; assumption. intros [[_ _] []]. intros [[a]]. destruct a. Qed. Theorem FunctionSpace: ∀x y, ∃ˢz, ∀w, w ∈ z ↔ is_function x y w. Proof. intros x y. setexists (x ⇛ y). apply tt. apply functionspacechar. Qed. Definition π₁ (x y:V): V := sup (x × y) (λ p, let (α, β) := p in 〈〈x α, y β〉, x α〉). Lemma π₁fun (x y: V): is_function (x × y) x (π₁ x y). Proof. repeat split. intros z [[α β] eq]. simpl in eq. exists ((α, β), α). assumption. intros [α β]. exists α. exists (α, β). apply refV. intros α β β'. intros [[[idx11 idx12] eq1] [[idx21 idx22] eq2]]. repeat match goal with [hyp: _ ≐ pV (π₁ x y) (?a, ?b) |- _] => change ((π₁ x y) (a, b)) with 〈〈x a, y b〉, x a〉 in hyp end. repeat match goal with [hyp: 〈_, _〉 ≐ 〈_, _〉 |- _] => apply pairing_injective in hyp; destruct hyp end. eapply traV in e1; [| apply symV; apply e]. apply pairing_injective in e1; destruct e1 as [eq _]. eauto using traV, symV. Qed. Definition compose_relV (x y z: V) (R S: V): V := {{ p ∈ x × z | ∃α ∈ x, ∃β ∈ y, ∃γ ∈ z, 〈α, β〉 ∈ R ∧ 〈β, γ〉 ∈ S ∧ 〈α, γ〉 ≐ p }}. Lemma composed_rel_is_relV {x y z: V} (R S: V) : is_rel x y R → is_rel y z S → is_rel x z (compose_relV x y z R S). Proof. intros _ _. split; auto. apply tt. apply sep_sub. intros w w' [α [β [γ [αRβ [βSγ eq]]]]] weqw'. exists α. exists β. exists γ. repeat split; try assumption. eauto using traV; assumption. Qed. (* Define a functor from V to the (E-)category of setoids *) Definition obfn: V → setoid. intro x. apply (Build_setoid x (λ a b, x a ≐ x b)); eauto using refV, symV, traV. Defined. Definition arfn (x y: V): (x ⇛ y) → (obfn x) ⇒ (obfn y). intros [f fext]. apply (Build_setoidmap (obfn x) (obfn y) f). simpl. assumption. Defined. (* Must now verify functoriality *) Definition id_index (x: V): x ⇛ x. exists (λ α, α). auto. Defined. Lemma id_index_identity (x: V): (x ⇛ x) (id_index x) ≐ identity x. Proof. split. intro α. apply (sigrejig (x × x)). exists (α, α). apply (sigrejig x). exists α. exists (refV _). apply refV. intros [[α β] [γ eq]]. exists γ. unfold projT1. apply symV, eq. Qed. Lemma functoriality_id (x: V): arfn x x (id_index x) ≈ idmap. Proof. intros α. simpl. apply refV. Qed. Definition compose_index (x y z: V): y ⇛ z → x ⇛ y → x ⇛ z. intros [f fext] [g gext]. exists (λ α, f (g α)). intros. apply fext. apply gext. assumption. Defined. Lemma functoriality_composition (x y z: V) (F: y ⇛ z) (G: x ⇛ y) : arfn x z (compose_index x y z F G) ≈ (arfn y z F) ∘ (arfn x y G). Proof. destruct F as [f fext]; destruct G as [g gext]. simpl. intro; apply refV. Qed. (* Finally, proofs that this functor is full and faithful *) Lemma faithful (x y: V) (F G: x ⇛ y): arfn x y F ≈ arfn x y G → (x ⇛ y) F ≐ (x ⇛ y) G. Proof. destruct F as [f fext]; destruct G as [g gext]. unfold arfn. intro feqg. simpl in feqg. split; intro α; exists α; apply pairing_extensional; apply refV || apply feqg. Qed. Lemma full (x y: V): ∀f: setoidmap (obfn x) (obfn y), ∃G: x ⇛ y, arfn x y G ≈ f. Proof. intros [f fext]. unfold functionspace. apply (sigrejig (x → y)). exists f. exists fext. simpl. intro; apply refV. Qed. (* The functor maps any singleton to a terminal setoid. This together with fact that both categories are generated by the terminal object, and the full faithfulness of the functors, yield that if obfn x is projective in setoids, then so is x in V. In other words if obfn x admits axiom of choice, then so does x. *) Definition canon1_map (x:V) : (obfn {{ x }}) ⇒ unit_setoid. apply (Build_setoidmap (obfn {{ x }}) unit_setoid (λ a, tt)). trivial. Defined. Definition canon2_map (x:V) : unit_setoid ⇒ (obfn {{ x }}). apply (Build_setoidmap unit_setoid (obfn {{ x }}) (λ a, tt)). intros. apply setoidrefl. Defined. Lemma singleton_to_terminal (x:V): ∃F:(obfn {{ x }}) ⇒ unit_setoid, ∃G:unit_setoid ⇒ (obfn {{ x }}), F ∘ G ≈ idmap ∧ G ∘ F ≈ idmap. Proof. exists (canon1_map x). exists (canon2_map x). split. intro. swesetoid. intro. swesetoid. apply refV. Qed. End CZFU. (* Fin *)