header{*Experiment on formalising the simplicial model in HOLZF*}
theory Simplicial_Model_HOLZF
imports
"~~/src/HOL/Cardinals/Cardinals"
"Category2/Yoneda"
begin
subsection{*HOLZF and a formalisation of the simplicial model*}
hide_const Field
lemma well_order_sets_iso_unique2:
assumes "Well_order r" and " Well_order r'" and "iso r r' f" and "iso r r' g " and "a ∈ Field r"
shows "f a = g a"
by (metis assms(1) assms(2) assms(3) assms(4) assms(5) embed_embedS_iso embed_unique)
lemma well_order_sets_iso_unique:
assumes "well_order_on A r" and "well_order_on B r'"
and "iso r r' f" and "iso r r' g " and "a ∈ A"
shows "f a = g a"
by (metis assms embed_embedS_iso embed_unique well_order_on_Field)
lemma well_order_sets_iso_unique_aux:
assumes "well_order_on A r" and "well_order_on B r'"
and "iso r r' (f n)" and "iso r r' (g n) " and "a ∈ A"
shows "f n a = g n a" by (simp add: well_order_sets_iso_unique[OF assms])
definition "Pi_ZF f A B = (∀x. x |∈|A --> f x |∈| B)"
definition "Func_ZF f A B = ((∀a. a |∈|A --> f a |∈| B) ∧ (∀a. (¬ (a |∈|A)) --> f a = undefined))"
locale simplicial_set =
fixes X::"nat => ZF"
and \<dd> :: "nat => nat => ZF => ZF"
and s :: "nat => nat => ZF => ZF"
assumes \<dd>_pi: "i≤q+1 --> Pi_ZF (\<dd> (q+1) i) (X (q+1)) (X q)"
and s_pi: "i≤q --> Pi_ZF (s q i) (X q) (X (q + 1))"
and condition1: "q≠0 ∧ i<j ∧ j ≤ q + 1 ∧ x |∈| X (q + 1) --> (\<dd> q i o \<dd> (q+1) j) x = (\<dd> q (j - 1) o \<dd> (q+1) i) x"
and condition2: "i≤j ∧ j≤q ∧ x |∈| X q --> (s (q + 1) i o s q j) x = (s (q+1) (j+1) o s q i) x"
and condition3: "i<j ∧ j≤q ∧ x |∈| X q --> (\<dd> (q + 1) i o s q j) x = (s (q - 1) (j - 1) o \<dd> q i) x"
and condition4: "j≤q ∧ x |∈| X q --> (\<dd> (q+1) (j+1) o s q j) x = x"
and condition5: "j≤q ∧ x |∈| X q --> (\<dd> (q+1) j o s q j) x = x"
and condition6: "i>j+1 ∧ i≤q ∧ x |∈| X q --> (\<dd> (q + 1) i o s q j) x = (s (q - 1) j o \<dd> q (i - 1)) x"
locale two_simplicial_sets = Y: simplicial_set Y \<dd>y sy + X: simplicial_set X \<dd>x sx
for Y::"nat => ZF"
and \<dd>y :: "nat => nat => ZF => ZF"
and sy :: "nat => nat => ZF => ZF"
and X::"nat => ZF"
and \<dd>x :: "nat => nat => ZF => ZF"
and sx :: "nat => nat => ZF => ZF"
begin
sublocale X_Y: two_simplicial_sets X \<dd>x sx Y \<dd>y sy by unfold_locales
definition "morphism f = (∀n. Func_ZF (f n) (Y n) (X n)
∧ (∀i x. i≤n+1 ∧ x |∈| Y (n+1) --> (f n o \<dd>y (n + 1) i) x = (\<dd>x (n + 1) i o f (n + 1)) x)
∧ (∀i x. i≤n ∧ x |∈| Y n --> (f (n + 1) o sy n i) x = (sx n i o f n) x))"
lemma Func_eq: "(f ∈ Func A B) = ((f ∈ A -> B) ∧ (∀x. x∉A --> f x = undefined))"
unfolding Func_def by auto
lemma morphism_Func:
assumes "morphism f"
shows "Func_ZF (f n) (Y n) (X n)"
using assms
unfolding morphism_def by simp
end
lemma morphism_Func_extended:
assumes Y1: "simplicial_set Y1 \<dd>y1 sy1"
and Y2: "simplicial_set Y2 \<dd>y2 sy2"
and m: "two_simplicial_sets.morphism Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 f"
shows "Func_ZF (f n) (Y1 n) (Y2 n)"
proof -
interpret Y1_Y2: two_simplicial_sets Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2
using Y1 Y2 unfolding two_simplicial_sets_def by simp
show ?thesis using m unfolding Y1_Y2.morphism_def by auto
qed
context two_simplicial_sets
begin
definition "well_ordered_morphism F = (let f=fst F; g=snd F in morphism f
∧ (∀n. (∀x. x |∈| (X n::ZF) --> (g n) x ∈ ({r. well_order_on {y::ZF. y |∈| Y n ∧ f n y = x} r}))))"
end
locale three_simplicial_sets =
X: simplicial_set X \<dd>x sx + Y1: simplicial_set Y1 \<dd>y1 sy1 + Y2: simplicial_set Y2 \<dd>y2 sy2
for X::"nat => ZF"
and \<dd>x :: "nat => nat => ZF => ZF"
and sx :: "nat => nat => ZF => ZF"
and Y1::"nat => ZF"
and \<dd>y1 :: "nat => nat => ZF => ZF"
and sy1 :: "nat => nat => ZF => ZF"
and Y2::"nat => ZF"
and \<dd>y2 :: "nat => nat => ZF => ZF"
and sy2 :: "nat => nat => ZF => ZF"
begin
sublocale Y1_X: two_simplicial_sets Y1 \<dd>y1 sy1 X \<dd>x sx by unfold_locales
sublocale Y2_X: two_simplicial_sets Y2 \<dd>y2 sy2 X \<dd>x sx by unfold_locales
sublocale Y1_Y2: two_simplicial_sets Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 by unfold_locales
definition "iso_between_morphism_weak f1 f2 g
= (Y1_X.well_ordered_morphism f1
∧ Y2_X.well_ordered_morphism f2 (*Both f1 and f2 are a well ordered morphism*)
∧ Y1_Y2.morphism g (*Morphism between simplicial set*)
∧ (∀n::nat. ∀y. y |∈| (Y1 n) --> (fst(f2) n) (g n y) = (fst(f1) n) y) (*Commute*)
∧ (∀n::nat. ∀x. x |∈| X n --> iso (snd f1 n x) (snd f2 n x) (g n)) (*Isomorphism between fibers that respects the well-order on them*)
)"
lemma iso_fibers_to_fibers:
assumes i: "iso_between_morphism_weak (f1,ord1) (f2,ord2) g"
shows "g n ∈ {y. y |∈| Y1 n ∧ f1 n y = x} -> {y. y |∈| Y2 n ∧ f2 n y = x}"
proof (unfold Pi_def, auto)
have gn_Pi: "(∀a. a |∈| Y1 n --> g n a |∈| Y2 n)"
using i unfolding iso_between_morphism_weak_def unfolding Y1_Y2.morphism_def Func_ZF_def by auto
fix xa assume xa_Y1: "xa |∈| Y1 n"
thus "f2 n (g n xa) = f1 n xa"
by (metis i fst_conv iso_between_morphism_weak_def)
show "g n xa |∈| Y2 n" using xa_Y1 gn_Pi by auto
qed
lemma iso_between_morphism_weak_unique':
assumes g: "iso_between_morphism_weak (f1,ord1) (f2,ord2) g"
and f: "iso_between_morphism_weak (f1,ord1) (f2,ord2) f"
and a: "a |∈| Y1 n"
shows "g n a = f n a"
proof -
def x≡"f1 n a"
have f1_Pi: "Pi_ZF (f1 n) (Y1 n) (X n)"
using g
unfolding iso_between_morphism_weak_def Y1_X.well_ordered_morphism_def Y1_X.morphism_def Func_ZF_def Pi_ZF_def by auto
have x: "x |∈| X n" unfolding x_def using f1_Pi a unfolding Pi_ZF_def by auto
show ?thesis
proof (rule well_order_sets_iso_unique_aux[of "{y. y |∈| Y1 n ∧ f1 n y = x}" "ord1 n x" "{y. y|∈|Y2 n ∧ f2 n y = x}" "(ord2 n x)" g n f a])
show "well_order_on {y. y |∈| Y1 n ∧ f1 n y = x} (ord1 n x)"
using f x Y1_X.well_ordered_morphism_def assms(2) iso_between_morphism_weak_def
unfolding iso_between_morphism_weak_def by auto
show "well_order_on {y. y|∈|Y2 n ∧ f2 n y = x} (ord2 n x)"
using g x Y2_X.well_ordered_morphism_def assms(2)
iso_between_morphism_weak_def unfolding iso_between_morphism_weak_def by auto
show "iso (ord1 n x) (ord2 n x) (g n)" by (metis g iso_between_morphism_weak_def snd_conv x)
show "iso (ord1 n x) (ord2 n x) (f n)" by (metis f iso_between_morphism_weak_def snd_conv x)
show " a ∈ {y. y |∈| Y1 n ∧ f1 n y = x}" by (metis (mono_tags, lifting) a mem_Collect_eq x_def)
qed
qed
lemma iso_between_morphism_weak_unique:
assumes g: "iso_between_morphism_weak (f1,ord1) (f2,ord2) g"
and f: "iso_between_morphism_weak (f1,ord1) (f2,ord2) f"
shows "g = f"
proof (rule+)
fix n a
show "g n a = f n a"
proof (cases "a |∈| Y1 n")
case True thus ?thesis using iso_between_morphism_weak_unique' f g by simp
next
case False
have "g n a = undefined" using g False
unfolding iso_between_morphism_weak_def morphism_def Func_ZF_def
by simp
moreover have "f n a = undefined" using f False
unfolding iso_between_morphism_weak_def morphism_def Func_ZF_def
by simp
ultimately show ?thesis ..
qed
qed
end
definition "compose_ZF A g f = (λx. if x |∈| A then g (f x) else undefined)"
definition "restrict_ZF f A = (λx. if x |∈| A then f x else undefined)"
definition "image_ZF f A = Repl A f"
definition "inj_on_ZF f A = (∀x y. x|∈|A ∧ y|∈|A ∧ f x = f y --> x = y)"
definition "bij_betw_ZF f A B = (inj_on_ZF f A ∧ image_ZF f A = B)"
context two_simplicial_sets
begin
definition "fiber x n f = {y. y |∈| Y n ∧ f n y = x}"
definition "simplicial_set_iso f = (morphism f
∧ (∃g. X_Y.morphism g ∧
(∀n. compose_ZF (X n) (f n) (g n) = restrict_ZF Fun.id (X n)
∧ compose_ZF (Y n) (g n) (f n) = restrict_ZF Fun.id (Y n))))"
lemma simplicial_set_iso_bij:
assumes f: "simplicial_set_iso f"
shows "bij_betw_ZF (f n) (Y n) (X n)"
proof (unfold bij_betw_ZF_def, auto simp add: image_ZF_def)
show" inj_on_ZF (f n) (Y n)" unfolding inj_on_ZF_def using assms unfolding simplicial_set_iso_def
unfolding compose_ZF_def restrict_ZF_def
by (auto, smt2 DEADID.map_id Func_ZF_def X_Y.morphism_Func local.morphism_Func)
next
have "(Repl (Y n) (f n)) |⊆| (X n)"
unfolding subset_def unfolding Repl
using assms unfolding simplicial_set_iso_def
unfolding morphism_def Func_ZF_def by auto
obtain g where g: "X_Y.morphism g"
and c: "(∀n. compose_ZF (X n) (f n) (g n) = restrict_ZF Fun.id (X n)
∧ compose_ZF (Y n) (g n) (f n) = restrict_ZF Fun.id (Y n))"
using f unfolding simplicial_set_iso_def by auto
moreover have "(X n) |⊆| (Repl (Y n) (f n))"
unfolding subset_def
proof auto
fix x assume x: "x |∈| X n"
have "∃a. a |∈| Y n ∧ x = f n a"
proof (rule exI[of _ "g n x"], rule conjI)
show "g n x |∈| Y n" using g x unfolding X_Y.morphism_def Func_ZF_def by auto
show " x = f n (g n x)" using c x unfolding compose_ZF_def restrict_ZF_def Fun.id_def fun_eq_iff
by metis
qed
thus "x |∈| Repl (Y n) (f n)"
unfolding Repl by simp
qed
ultimately show "Repl (Y n) (f n) = X n" by (metis Ext `Repl (Y n) (f n) |⊆| X n` subset_def)
qed
end
context two_simplicial_sets
begin
lemma simplicial_set_iso_g:
assumes s: "simplicial_set_iso f"
obtains g where "X_Y.simplicial_set_iso g"
and "(∀n. compose_ZF (X n) (f n) (g n) = restrict_ZF Fun.id (X n) ∧ compose_ZF (Y n) (g n) (f n) = restrict_ZF Fun.id (Y n))"
proof -
obtain g where g: "X_Y.morphism g"
and g2: "(∀n. compose_ZF (X n) (f n) (g n) = restrict_ZF Fun.id (X n)
∧ compose_ZF (Y n) (g n) (f n) = restrict_ZF Fun.id (Y n))"
using s unfolding simplicial_set_iso_def by auto
with that show ?thesis by (metis X_Y.simplicial_set_iso_def local.simplicial_set_iso_def s)
qed
end
context three_simplicial_sets
begin
definition "iso_between_morphism f1 f2 g
= (Y1_X.well_ordered_morphism f1
∧ Y2_X.well_ordered_morphism f2 (*Both f1 and f2 are a well ordered morphism*)
∧ Y1_Y2.simplicial_set_iso g (*Isomorphism between simplicial set*)
∧ (∀n::nat. ∀y. y |∈| Y1 n --> (fst(f2) n) (g n y) = (fst(f1) n) y) (*Commute*)
∧ (∀n::nat. ∀x. x |∈| X n --> iso (snd f1 n x) (snd f2 n x) (g n)) (*Isomorphism between fibers that respects the well-order on them*)
)"
lemma iso_imp_iso_weak:
assumes "iso_between_morphism f1 f2 g"
shows "iso_between_morphism_weak f1 f2 g"
using assms
unfolding iso_between_morphism_def iso_between_morphism_weak_def simplicial_set_iso_def
by auto
lemma iso_between_morphism_unique':
assumes g: "iso_between_morphism (f1,ord1) (f2,ord2) g"
and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
and a: "a |∈| Y1 n"
shows "g n a = f n a"
using iso_between_morphism_weak_unique'[OF _ _ a]
using iso_imp_iso_weak[OF f] iso_imp_iso_weak[OF g]
by auto
corollary iso_between_morphism_unique:
assumes g: "iso_between_morphism (f1,ord1) (f2,ord2) g"
and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
shows "g = f"
proof (rule+)
fix n a
show "g n a = f n a"
proof (cases "a |∈| Y1 n")
case True thus ?thesis using iso_between_morphism_unique' g f by simp
next
case False
have "g n a = undefined"
using g False
unfolding iso_between_morphism_def simplicial_set_iso_def morphism_def Func_ZF_def
by simp
moreover have "f n a = undefined"
using f False
unfolding iso_between_morphism_def simplicial_set_iso_def morphism_def Func_ZF_def
by simp
ultimately show ?thesis ..
qed
qed
end
context two_simplicial_sets
begin
text{*The product $Y \times X$ is a simplicial set*}
sublocale simplicial_set_prod:
simplicial_set "(λn. (Y n) |×| (X n)) "
"(λi n x. Opair (\<dd>y i n (Fst x)) (\<dd>x i n (Snd x)))"
"(λi n x. Opair (sy i n (Fst x)) (sx i n (Snd x)))"
proof (unfold simplicial_set_def, auto simp add: Pi_ZF_def)
fix i q yx
assume i: "i ≤ Suc q" and yx: "yx |∈| Y (Suc q) |×| X (Suc q)"
let ?y="Fst yx"
let ?x="Snd yx"
have y: "?y |∈| Y (Suc q)" and x: "?x |∈| X (Suc q) ∧ isOpair yx"
using yx ZFCartProd by auto
show "Opair (\<dd>y (Suc q) i ?y) (\<dd>x (Suc q) i ?x) |∈| Y q |×| X q"
proof (unfold CartProd, rule exI[of _ "\<dd>y (Suc q) i ?y"], rule exI[of _ "\<dd>x (Suc q) i ?x"], auto)
show "\<dd>y (Suc q) i (Fst yx) |∈| Y q" using Y.\<dd>_pi i y unfolding Pi_ZF_def by auto
show "\<dd>x (Suc q) i (Snd yx) |∈| X q" using X.\<dd>_pi i x unfolding Pi_ZF_def by auto
qed
next
fix i q x
assume i: "i ≤ q" and x: "x |∈| Y q |×| X q"
show "Opair (sy q i (Fst x)) (sx q i (Snd x)) |∈| Y (Suc q) |×| X (Suc q)"
proof (unfold CartProd, rule exI[of _ "(sy q i (Fst x))"], rule exI[of _ "(sx q i (Snd x))"], auto)
show "sy q i (Fst x) |∈| Y (Suc q)" using Y.s_pi i ZFCartProd[OF x] unfolding Pi_ZF_def by auto
show "sx q i (Snd x) |∈| X (Suc q)" using X.s_pi i ZFCartProd[OF x] unfolding Pi_ZF_def by simp
qed
next
fix q i j yx
assume q: "0 < q" and ij: "i < j" and j: "j ≤ Suc q"
and yx: "yx |∈| Y (Suc q) |×| X (Suc q)"
let ?y="Fst yx"
let ?x="Snd yx"
have y: "?y |∈| Y (Suc q)" and x: "?x |∈| X (Suc q)"
using yx ZFCartProd by auto
show "Opair (\<dd>y q i (Fst (Opair (\<dd>y (Suc q) j (?y)) (\<dd>x (Suc q) j (?x)))))
(\<dd>x q i (Snd (Opair (\<dd>y (Suc q) j (?y)) (\<dd>x (Suc q) j (?x))))) =
Opair (\<dd>y q (j - Suc 0) (Fst (Opair (\<dd>y (Suc q) i (?y)) (\<dd>x (Suc q) i (?x)))))
(\<dd>x q (j - Suc 0) (Snd (Opair (\<dd>y (Suc q) i (?y)) (\<dd>x (Suc q) i (?x)))))"
unfolding Fst Snd Opair
using Y.condition1 X.condition1 y x q ij j by auto
next
fix i j q x
assume "i ≤ j" and "j ≤ q" and x: "x |∈| Y q |×| X q"
moreover have Fst_x: "Fst x |∈| Y q" and Snd_x: "Snd x |∈| X q"
using ZFCartProd[OF x] by auto
ultimately show "Opair (sy (Suc q) i (Fst (Opair (sy q j (Fst x)) (sx q j (Snd x))))) (sx (Suc q) i (Snd (Opair (sy q j (Fst x)) (sx q j (Snd x))))) =
Opair (sy (Suc q) (Suc j) (Fst (Opair (sy q i (Fst x)) (sx q i (Snd x))))) (sx (Suc q) (Suc j) (Snd (Opair (sy q i (Fst x)) (sx q i (Snd x)))))"
unfolding Fst Snd Opair
using Y.condition2 X.condition2 by auto
next
fix i j q x
assume "i < j" and "j ≤ q" and "x |∈| Y q |×| X q"
moreover hence Fst_x: "Fst x |∈| Y q" and Snd_x: "Snd x |∈| X q"
using ZFCartProd by auto
ultimately show "Opair (\<dd>y (Suc q) i (Fst (Opair (sy q j (Fst x)) (sx q j (Snd x))))) (\<dd>x (Suc q) i (Snd (Opair (sy q j (Fst x)) (sx q j (Snd x))))) =
Opair (sy (q - Suc 0) (j - Suc 0) (Fst (Opair (\<dd>y q i (Fst x)) (\<dd>x q i (Snd x)))))
(sx (q - Suc 0) (j - Suc 0) (Snd (Opair (\<dd>y q i (Fst x)) (\<dd>x q i (Snd x)))))"
unfolding Fst Snd Opair
using Y.condition3 X.condition3 by auto
next
fix j q x
assume "j ≤ q" and "x |∈| Y q |×| X q"
moreover hence Fst_x: "Fst x |∈| Y q" and Snd_x: "Snd x |∈| X q" and is_Opair_x: "isOpair x"
using ZFCartProd by auto
ultimately show "Opair (\<dd>y (Suc q) (Suc j) (Fst (Opair (sy q j (Fst x)) (sx q j (Snd x)))))
(\<dd>x (Suc q) (Suc j) (Snd (Opair (sy q j (Fst x)) (sx q j (Snd x))))) = x"
unfolding Fst Snd
using Y.condition4 X.condition4 FstSnd[OF is_Opair_x] by auto
next
fix j q x assume "j ≤ q" and "x |∈| Y q |×| X q"
moreover hence Fst_x: "Fst x |∈| Y q" and Snd_x: "Snd x |∈| X q" and is_Opair_x: "isOpair x"
using ZFCartProd by auto
ultimately show "Opair (\<dd>y (Suc q) j (Fst (Opair (sy q j (Fst x)) (sx q j (Snd x)))))
(\<dd>x (Suc q) j (Snd (Opair (sy q j (Fst x)) (sx q j (Snd x))))) = x"
unfolding Fst Snd
using Y.condition5 X.condition5 FstSnd[OF is_Opair_x] by auto
next
fix j i q x
assume "Suc j < i" and "i ≤ q" and "x |∈| Y q |×| X q"
moreover hence Fst_x: "Fst x |∈| Y q" and Snd_x: "Snd x |∈| X q" and is_Opair_x: "isOpair x"
using ZFCartProd by auto
ultimately show "Opair (\<dd>y (Suc q) i (Fst (Opair (sy q j (Fst x)) (sx q j (Snd x))))) (\<dd>x (Suc q) i (Snd (Opair (sy q j (Fst x)) (sx q j (Snd x))))) =
Opair (sy (q - Suc 0) j (Fst (Opair (\<dd>y q (i - Suc 0) (Fst x)) (\<dd>x q (i - Suc 0) (Snd x)))))
(sx (q - Suc 0) j (Snd (Opair (\<dd>y q (i - Suc 0) (Fst x)) (\<dd>x q (i - Suc 0) (Snd x)))))"
unfolding Fst Snd Opair
using Y.condition6 X.condition6 by auto
qed
lemma "simplicial_set (λn. (Y n) |×| (X n))
(λi n x. Opair (\<dd>y i n (Fst x)) (\<dd>x i n (Snd x)))
(λi n x. Opair (sy i n (Fst x)) (sx i n (Snd x)))"
by unfold_locales
end
text{*The product $(Y \times_{tf} X)$ is a simplicial set*}
locale three_simplicial_sets_tf = Y1_Y2_X: three_simplicial_sets
+ fixes t and f
assumes t: "Y1_X.morphism t"
and f: "Y2_X.morphism f"
begin
sublocale Y1_times_Y2_tf: simplicial_set
"(λn. Sep (Y1 n |×| Y2 n) (λx. t n (Fst x) = f n (Snd x)))"
"(λi n x. Opair (\<dd>y1 i n (Fst x)) (\<dd>y2 i n (Snd x)))"
"(λi n x. Opair (sy1 i n (Fst x)) (sy2 i n (Snd x)))"
proof (unfold simplicial_set_def, auto simp add: Pi_ZF_def Sum image_def Fst Snd)
fix i q x
assume iq: "i ≤ Suc q"
and "x |∈| Sep (Y1 (Suc q) |×| Y2 (Suc q)) (λx. t (Suc q) (Fst x) = f (Suc q) (Snd x))"
hence yx: "x |∈|(Y1 (Suc q) |×| Y2 (Suc q))" and ta_fb: " t (Suc q) (Fst x) = f (Suc q) (Snd x)"
using Sep by auto
let ?a="Fst x"
let ?b="Snd x"
have a: "?a |∈| Y1 (Suc q)" and b: "?b |∈| Y2 (Suc q)"
using yx ZFCartProd by auto
show "Opair (\<dd>y1 (Suc q) i (Fst x)) (\<dd>y2 (Suc q) i (Snd x)) |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x))"
unfolding Sep Snd Fst
proof (auto)
have "t q (\<dd>y1 (Suc q) i ?a) = \<dd>x (q + 1) i (t (q + 1) ?a)"
using t iq a
unfolding Y1_X.morphism_def o_def unfolding Suc_eq_plus1 by metis
also have "... = \<dd>x (q + 1) i (f (Suc q) ?b)" using ta_fb by auto
also have "... = f q (\<dd>y2 (Suc q) i ?b)" using f iq b
unfolding Y2_X.morphism_def o_def unfolding Suc_eq_plus1 by metis
finally show "t q (\<dd>y1 (Suc q) i ?a) = f q (\<dd>y2 (Suc q) i ?b)" .
show "Opair (\<dd>y1 (Suc q) i (Fst x)) (\<dd>y2 (Suc q) i (Snd x)) |∈| Y1 q |×| Y2 q"
by (metis (erased , lifting) Pi_ZF_def Suc_eq_plus1 Y1_Y2.simplicial_set_prod.\<dd>_pi iq yx)
qed
next
fix i q x
assume iq: "i ≤ q"
and "x |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x))"
hence yx: "x |∈|(Y1 q |×| Y2 q)" and ta_fb: "t q (Fst x) = f q (Snd x)"
using Sep by auto
let ?a="Fst x"
let ?b="Snd x"
have a: "?a |∈| Y1 q" and b: "?b |∈| Y2 q"
using yx ZFCartProd by auto
show "Opair (sy1 q i (Fst x)) (sy2 q i (Snd x)) |∈| Sep (Y1 (Suc q) |×| Y2 (Suc q)) (λx. t (Suc q) (Fst x) = f (Suc q) (Snd x))"
unfolding Sep Snd Fst
proof (auto)
have "t (Suc q) (sy1 q i ?a) = sx q i (t q ?a)"
using t iq a unfolding Y1_X.morphism_def o_def unfolding Suc_eq_plus1 by metis
also have "... = sx q i (f q ?b)" unfolding ta_fb ..
also have "... = f (Suc q) (sy2 q i ?b)"
using f iq b unfolding Y2_X.morphism_def o_def unfolding Suc_eq_plus1 by metis
finally show "t (Suc q) (sy1 q i ?a) = f (Suc q) (sy2 q i ?b)" .
show "Opair (sy1 q i (Fst x)) (sy2 q i (Snd x)) |∈| Y1 (Suc q) |×| Y2 (Suc q)"
by (metis (erased , lifting) Pi_ZF_def Suc_eq_plus1 Y1_Y2.simplicial_set_prod.s_pi iq yx)
qed
next
fix q i j x
assume q: "0 < q"
and ij: "i < j"
and j: "j ≤ Suc q"
and yx: "x |∈| Sep (Y1 (Suc q) |×| Y2 (Suc q)) (λx. t (Suc q) (Fst x) = f (Suc q) (Snd x))"
hence "x |∈|(Y1 (Suc q) |×| Y2 (Suc q))" and ta_fb: "t (Suc q) (Fst x) = f (Suc q) (Snd x)"
using Sep by auto
hence a: "Fst x |∈| Y1 (Suc q)" and b: "Snd x |∈| Y2 (Suc q)"
using yx ZFCartProd by auto
thus "Opair (\<dd>y1 q i (\<dd>y1 (Suc q) j (Fst x))) (\<dd>y2 q i (\<dd>y2 (Suc q) j (Snd x)))
= Opair (\<dd>y1 q (j - Suc 0) (\<dd>y1 (Suc q) i (Fst x))) (\<dd>y2 q (j - Suc 0) (\<dd>y2 (Suc q) i (Snd x)))"
unfolding Opair using a b ij q j Y1.condition1 Y2.condition1 by auto
next
fix i j q x
assume i: "i ≤ j" and q: "j ≤ q"
and yx: "x |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x))"
hence "x |∈|(Y1 q |×| Y2 q)" and ta_fb: "t q (Fst x) = f q (Snd x)"
using Sep by auto
hence a: "Fst x |∈| Y1 q" and b: "Snd x |∈| Y2 q"
using yx ZFCartProd by auto
show "Opair (sy1 (Suc q) i (sy1 q j (Fst x))) (sy2 (Suc q) i (sy2 q j (Snd x))) =
Opair (sy1 (Suc q) (Suc j) (sy1 q i (Fst x))) (sy2 (Suc q) (Suc j) (sy2 q i (Snd x)))"
unfolding Opair
using a b i q Y1.condition2 Y2.condition2 by auto
next
fix i j q x
assume i: "i < j" and q: "j ≤ q"
and yx: "x |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x))"
hence "x |∈|(Y1 q |×| Y2 q)" and ta_fb: "t q (Fst x) = f q (Snd x)"
using Sep by auto
hence a: "Fst x |∈| Y1 q" and b: "Snd x |∈| Y2 q"
using yx ZFCartProd by auto
show "Opair (\<dd>y1 (Suc q) i (sy1 q j (Fst x))) (\<dd>y2 (Suc q) i (sy2 q j (Snd x))) =
Opair (sy1 (q - Suc 0) (j - Suc 0) (\<dd>y1 q i (Fst x))) (sy2 (q - Suc 0) (j - Suc 0) (\<dd>y2 q i (Snd x)))"
unfolding Opair
using a b i q Y1.condition3 Y2.condition3 by auto
next
fix i j q x
assume q: "j ≤ q"
and yx: "x |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x))"
hence "x |∈|(Y1 q |×| Y2 q)" and ta_fb: "t q (Fst x) = f q (Snd x)"
using Sep by auto
hence a: "Fst x |∈| Y1 q" and b: "Snd x |∈| Y2 q" and is_Opair_x: "isOpair x"
using yx ZFCartProd by auto
show "Opair (\<dd>y1 (Suc q) (Suc j) (sy1 q j (Fst x))) (\<dd>y2 (Suc q) (Suc j) (sy2 q j (Snd x))) = x"
and "Opair (\<dd>y1 (Suc q) j (sy1 q j (Fst x))) (\<dd>y2 (Suc q) j (sy2 q j (Snd x))) = x"
using Y1.condition4 Y2.condition4 Y1.condition5 Y2.condition5 FstSnd[OF is_Opair_x] q a b by auto
next
fix j i q x
assume j: "Suc j < i" and i: "i ≤ q"
and yx:"x |∈| Sep (Y1 q |×| Y2 q) (λx. t q (Fst x) = f q (Snd x)) "
hence "x |∈|(Y1 q |×| Y2 q)" and ta_fb: "t q (Fst x) = f q (Snd x)"
using Sep by auto
hence a: "Fst x |∈| Y1 q" and b: "Snd x |∈| Y2 q" and is_Opair_x: "isOpair x"
using yx ZFCartProd by auto
show "Opair (\<dd>y1 (Suc q) i (sy1 q j (Fst x))) (\<dd>y2 (Suc q) i (sy2 q j (Snd x))) =
Opair (sy1 (q - Suc 0) j (\<dd>y1 q (i - Suc 0) (Fst x))) (sy2 (q - Suc 0) j (\<dd>y2 q (i - Suc 0) (Snd x)))"
unfolding Opair
using j i a b Y1.condition6 Y2.condition6 by auto
qed
end
end