Theory Simplicial_Model_HOL

(*
  Title: Simplicial_Model_HOL
  Author: Jose Divasón <jose.divasonm@unirioja.es>
*)

header "Simplicial Sets"

theory Simplicial_Model_HOL
  imports
  "~~/src/HOL/Cardinals/Cardinals"
  "~~/src/HOL/Library/FuncSet"
begin

text{*Voevodsky's simplicial model: \url{http://arxiv.org/abs/1203.2553}*}

subsection "Simplicial sets and morphisms"

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)

text{*The following definition models simplicial sets. Since the elements do not
  belong to a unique $n$ (that is, $x$ could belong to $X_n$ and to $X_m$, then I have to add
  a parameter (the grade) to each function. 

  Really, the symbol that is commonly used to refer the faces is @{text "∂"}, but
  in Isabelle is not allowed in the name of a function, thus I use  @{text "\<dd>"} instead.*}

(*
  My first trial was:

  class simplicial_set = 
  fixes X::"nat => 'a set" 
  and \<dd> :: "nat => nat => 'a => 'a"
  and s :: "nat => nat => 'a => 'a"
  assumes \<dd>_pi: "i≤q+1 --> \<dd> (q+1) i ∈ X (q+1) -> X q"
  and s_pi: "i≤q --> s q i ∈ X q -> X (q + 1)"
  and condition1: "q≠0 ∧ i<j ∧ j ≤ q + 1 --> \<dd> q i o \<dd> (q+1) j = \<dd> q (j - 1) o \<dd> (q+1) i"
  and condition2: "i≤j ∧ j≤q --> s (q + 1) i o s q j = s (q+1) (j+1) o s q i"
  and condition3: "i<j ∧ j≤q --> \<dd> (q + 1) i o s q j= s (q - 1) (j - 1) o \<dd> q i"
  and condition4: "j≤q --> \<dd> (q+1) (j+1) o s q j = id"
  and condition5: "j≤q --> \<dd> (q+1) j o s q j = id"
  and condition6: "i>j+1 ∧ i≤q --> \<dd> (q + 1) i o s q j = s (q - 1) j o \<dd> q (i - 1)" 

  But I had problems with the compositions outside the domain, specially when trying to 
  prove from_sSet as a functor (in a side I had the identity restricted to the domain and I had to 
  prove that such a function was equal to the identity). So I had to change the definitions and use 
  compose, Func … to take care of the domain.
*)

class simplicial_set = 
  fixes X::"nat => 'a set" 
  and \<dd> :: "nat => nat => 'a => 'a"
  and s :: "nat => nat => 'a => 'a"
  assumes \<dd>_pi: "i≤q+1 --> \<dd> (q+1) i ∈ X (q+1) -> X q"
  and s_pi: "i≤q --> 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" (*q is not allowed to be 0*)
  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 => 'b set" 
  and \<dd>y :: "nat => nat => 'b => 'b"
  and sy :: "nat => nat => 'b => 'b"
  and X::"nat => 'a set" 
  and \<dd>x :: "nat => nat => 'a => 'a"
  and sx :: "nat => nat => 'a => 'a" 
begin

sublocale X_Y: two_simplicial_sets X \<dd>x sx Y \<dd>y sy  by unfold_locales

(*Due to the same reason why we have changed the definition of simplicial set, we have 
  had to add here conditions about the domain.
  In addition, we have to impose Func (undefined outside the domain) and not only Pi 
  (with only Pi it does not work properly in future demonstratios)
*)

(*
Some previous trials were:
*)

(*
  definition "morphism f = (∀n. f n ∈ (Y n) -> (X n) 
  ∧ (∀i. i≤n --> f n o \<dd>y (n + 1) i = \<dd>x (n + 1) i o f (n + 1)
  ∧ f (n + 1) o sy n i = sx n i o f n))"
*)

(*
  definition "morphism f = (∀n. f n ∈ (Y n) -> (X n) 
  ∧ (∀i. i≤n+1 --> f n o \<dd>y (n + 1) i = \<dd>x (n + 1) i o f (n + 1))
  ∧ (∀i. i≤n --> f (n + 1) o sy n i = sx n i o f n))"
*)
(*
  definition "morphism f = (∀n. 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))"
*)

definition "morphism f = (∀n. f n ∈ Func (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 "f n ∈ Func (Y n) (X n)"
  using assms
  unfolding morphism_def by simp

end

lemma morphism_Func_extended: 
  assumes Y1: "class.simplicial_set Y1 \<dd>y1 sy1" 
  and Y2: "class.simplicial_set Y2 \<dd>y2 sy2" 
  and m: "two_simplicial_sets.morphism Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 f"
  shows "f n ∈ Func (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

subsection{*Well-ordered morphisms*}

context two_simplicial_sets
begin


text{*In the fiber, I have to assume that @{text "y ∈ Y n"}. If not, it might exist an element
  @{text "y"} such that @{text "y ∉ Y n ∧ f n y = x"}*}

(*NOTA: Antes la había definido así:
  Note: Previously, I had defined it as follows:

  definition "well_ordered_morphism F = (let f=fst F; g=snd F in morphism f 
  ∧ (∀n. g ∈ Pi (X n::'a set) (%x. {r. well_order_on {y::'b. y ∈ Y n ∧ f n y = x} r})))"

  But g must be parameterized by n, otherwise I cannot prove:

  lemma Y1_times_Y2_tf_Y1_well_ordered_morphism_fst: 
  shows "X_Y1_Y2_tf.Y1_times_Y2_tf_Y1.well_ordered_morphism
  ((λn x. fst x), 
  (λn y1. {((a,b),(c,d)). fst (a,b) = y1 ∧ fst (c,d) = y1 
  ∧  (a,b) ∈ {(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2} 
  ∧ (c,d) ∈ {(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2} 
  ∧ (b,d) ∈ ord (t n y1)}))"   

  Since it appears the premisse a ∈ Y1 n and I have to demonstrate it belongs to Y1 m as well.
*)

definition "well_ordered_morphism F = (let f=fst F; g=snd F in morphism f 
  ∧ (∀n. g n ∈ Pi (X n::'a set) (%x. {r. well_order_on {y::'b. 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 => 'a set" 
  and \<dd>x :: "nat => nat => 'a => 'a"
  and sx :: "nat => nat => 'a => 'a"
  and Y1::"nat => 'b set" 
  and \<dd>y1 :: "nat => nat => 'b => 'b"
  and sy1 :: "nat => nat => 'b => 'b"
  and Y2::"nat => 'c set" 
  and \<dd>y2 :: "nat => nat => 'c => 'c"
  and sy2 :: "nat => nat => 'c => 'c"
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

(*
  The following definition is different to the one presented in the Voevodsky's simplicial model.
  He imposes there exists an isomorphism between the simplicial sets Y1 and Y2. I have just imposed 
  there exists an morphism.
*)

(*
  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. (fst(f2) n) o (g n) = (fst(f1) n)) (*Commute*)
  ∧ (∀n::nat. ∀x ∈ X n. iso (snd f1 x) (snd f2 x) (g n)) (*Isomorphism between fibers that respects the well-order on them*)
  )"
*)

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 morphisms*)
  ∧ Y1_Y2.morphism g (*Morphism between simplicial sets*)
  ∧ (∀n::nat. ∀y ∈ Y1 n. (fst(f2) n) (g n y) = (fst(f1) n) y) (*Commute*)
  ∧ (∀n::nat. ∀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: "g n ∈ Y1 n -> Y2 n" 
    using i unfolding iso_between_morphism_weak_def unfolding Y1_Y2.morphism_def Func_def by auto
  fix xa assume xa_Y1: "xa ∈ Y1 n" and "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: "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_def by auto 
  have x: "x ∈ X n" unfolding x_def using f1_Pi a by auto 
  show ?thesis
  proof (rule well_order_sets_iso_unique[of "{y∈Y1 n. f1 n y = x}" "ord1 n x"]) 
    show "well_order_on {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 "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 ∈ Y1 n. f1 n y = x}" by (metis (mono_tags, lifting) a mem_Collect_eq x_def)
    show "well_order_on {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
  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_def
      by simp
    moreover have "f n a = undefined" using f False 
      unfolding iso_between_morphism_weak_def morphism_def Func_def
      by simp
    ultimately show ?thesis ..
  qed
qed

end

subsection{*Simplicial set isomorphism*}

context two_simplicial_sets
begin

(* x must belong to X n. f must be a morphism. *)
definition "fiber x n f = {y∈Y n. f n y = x}"

(*Definition 4*)
(* α and f could be fixed in a locale *)
definition "α_small α f = (Card_order α ∧ regularCard α ∧ morphism f 
  ∧ (∀n. ∀x ∈ X n. |fiber x n f| <o α))"

text{*Isomorphism between simplicial sets*}

(*
  definition "simplicial_set_iso f = (morphism f
  ∧ (∃g. X_Y.morphism g
  ∧ (∀n. (f n) o (g n) = id ∧ (g n) o (f n) = id)))"*)

(*We had to change the definition and impose conditions about the domain*)

(*
  definition "simplicial_set_iso f = (morphism f
  ∧ (∃g. X_Y.morphism g ∧
  (∀n. (f n) o (g n) = id ∧ (g n) o (f n) = id)))"
*)

definition "simplicial_set_iso f = (morphism f
  ∧ (∃g. X_Y.morphism g ∧
  (∀n. compose (X n) (f n) (g n) = restrict id (X n) 
  ∧ compose (Y n) (g n) (f n) = restrict id (Y n))))"

text{*Isomorphism between simplicial sets preserving the well-orders between Y and X.*}

(*Another possible definition would be that it respects the well-orders in the fibers.*)

definition "simplicial_set_wo_iso f = (simplicial_set_iso f
  ∧ (∀r n.  Well_order r ∧ (Field r = Y n) --> (∃r'. Well_order r' ∧ (Field r' = (X n)) ∧ iso r r' (f n))))"

(*The inverse also respects well-orders.*)
definition "simplicial_set_wo_iso2 f = (morphism f
  ∧ (∃g. X_Y.morphism g
  ∧ (∀n. compose (X n) (f n) (g n) = restrict id (X n) ∧ compose (Y n) (g n) (f n) = restrict id (Y n))
  ∧ (∀r n. Well_order r ∧ Field r = X n --> (∃r'. Well_order r' ∧ (Field r' = (Y n)) ∧ iso r r' (g n))))
  ∧ (∀r n. Well_order r ∧ Field r = Y n --> (∃r'. Well_order r' ∧ (Field r' = (X n)) ∧ iso r r' (f n))))"


lemma simplicial_set_iso_bij:
  assumes "simplicial_set_iso f"
  shows "bij_betw (f n) (Y n) (X n)"
proof (unfold bij_betw_def, auto)
  show" inj_on (f n) (Y n)" unfolding inj_on_def using assms unfolding simplicial_set_iso_def 
    unfolding compose_def restrict_def by (metis id_apply)
  fix xa assume xa: "xa ∈ Y n" thus "f n xa ∈ X n"
    using assms xa
    unfolding simplicial_set_iso_def local.morphism_def Func_def
    by fast  
next 
  fix x assume "x ∈ X n" thus "x ∈ f n ` Y n"
    using assms unfolding simplicial_set_iso_def
    unfolding X_Y.morphism_def image_iff compose_def restrict_def
    by (metis (erased, hide_lams) Func_elim id_apply)  
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. (f n) o (g n) = id ∧ (g n) o (f n) = id)"*)
  and "(∀n. compose (X n) (f n) (g n) = restrict id (X n) 
  ∧ compose (Y n) (g n) (f n) = restrict id (Y n))"
proof -
  obtain g where g: "X_Y.morphism g" 
    and g2: "(∀n. compose (X n) (f n) (g n) = restrict id (X n) 
    ∧ compose (Y n) (g n) (f n) = restrict 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


lemma ss_wo_iso_imp_ss_wo_iso2:
  assumes s: "simplicial_set_wo_iso f"
  shows "simplicial_set_wo_iso2 f"
proof (unfold simplicial_set_wo_iso2_def, auto)
  show "morphism f" using s unfolding simplicial_set_wo_iso_def simplicial_set_iso_def by simp
  fix r n assume "well_order_on (Y n) r" and "Field r = Y n"
  thus "∃r'. Well_order r' ∧ Field r' = X n ∧ iso r r' (f n)" 
    using s unfolding simplicial_set_wo_iso_def by auto
next
  obtain g where g1: "X_Y.morphism g"
    and g2: "(∀n. compose (X n) (f n) (g n) = restrict id (X n) 
    ∧ compose (Y n) (g n) (f n) = restrict id (Y n))"
    using s unfolding simplicial_set_wo_iso_def simplicial_set_iso_def by auto
  show "∃g. X_Y.morphism g ∧
    (∀n. compose (X n) (f n) (g n) = restrict id (X n) 
    ∧ compose (Y n) (g n) (f n) = restrict id (Y n)) 
    ∧ (∀r n. Well_order r ∧ Field r = X n 
    --> (∃r'. Well_order r' ∧ Field r' = Y n ∧ iso r r' (g n)))"
  proof (rule exI[of _ g], auto, auto simp add: g1 g2)
    fix r n assume wo_r: "well_order_on (X n) r" and Xn: "Field r = X n"
    hence Wo_r: "Well_order r" by auto
    have gn_Pi: "g n ∈ X n -> Y n" using g1 unfolding X_Y.morphism_def Func_def by simp
    have fn_Pi: "f n ∈ Y n -> X n" 
      using s
      unfolding simplicial_set_wo_iso_def simplicial_set_iso_def morphism_def Func_def by simp
    def r'=="{(g n a, g n b)|a b. (a,b) ∈ r}"
    have r'_subset_Yn: "Field r' ⊆ Y n"
    proof 
      fix y assume "y ∈ Field r'" thus "y ∈ Y n" using gn_Pi unfolding r'_def Field_def
        by auto (metis funcset_mem well_order_on_domain wo_r)+
    qed
    have Wo_r': "Well_order r'"
    proof (unfold well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def, auto)
      have R_r: "Refl r" 
        using Wo_r
        by (metis linear_order_on_def order_on_defs(1) partial_order_on_def well_order_on_def)
      show R_r': "Refl r'"
        unfolding r'_def refl_on_def Field_def Domain_fst Range_snd image_def
      proof auto
        fix a ba assume *: "(a, ba) ∈ r"
        show "∃aa. g n a = g n aa ∧ (∃b. g n a = g n b ∧ (aa, b) ∈ r)"
          by (rule exI[of _ a], simp, rule exI[of _ a], metis R_r * refl_onD refl_on_domain) 
      next
        fix a b assume *: "(a, b) ∈ r"
        show "∃a. g n b = g n a ∧ (∃ba. g n b = g n ba ∧ (a, ba) ∈ r)"
          by (rule exI[of _ b], simp, rule exI[of _ b], metis R_r * refl_onD refl_on_domain)
      qed
      have trans_r: "trans r" 
        using Wo_r 
        unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by simp
      show trans_r': "trans r'"
        unfolding r'_def trans_def
      proof auto
        fix a b aa ba
        assume 1: "(a, b) ∈ r" and 2: "g n b = g n aa" and 3: "(aa, ba) ∈ r" 
        have "f n (g n b) = f n (g n aa)" using 2 by simp
        hence b_eq_aa: "b = aa" 
          using g2 unfolding compose_def restrict_def
          by (metis "1" "3" id_apply well_order_on_domain wo_r)
        show "∃aa. g n a = g n aa ∧ (∃b. g n ba = g n b ∧ (aa, b) ∈ r)"
        proof (rule exI[of _ a], simp, rule exI[of _ ba], simp)
          show "(a, ba) ∈ r" using trans_r unfolding trans_def using 1 3 unfolding b_eq_aa by blast
        qed
      qed
      have antisym_r: "antisym r"
        using Wo_r 
        unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by simp
      show antisym_r': "antisym r'" 
        unfolding r'_def antisym_def
      proof auto
        fix a b aa ba assume 1: "(a, b) ∈ r" and 2: "g n b = g n aa" and 3: "g n a = g n ba"
          and 4: "(aa, ba) ∈ r"
        have "f n (g n b) = f n (g n aa)" and "f n (g n a) = f n (g n ba)" using 2 3 by auto
        hence b_aa: "b=aa" and a_ba: "a=ba" using g2 unfolding compose_def restrict_def
          by (metis "1" "4" id_apply well_order_on_domain wo_r)+          
        show "g n ba = g n aa"
          using antisym_r unfolding antisym_def using 1 4 unfolding b_aa a_ba by blast
      qed
      have Total_r: "Total r" using Wo_r 
        unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by simp
      show Total_r': "Total r'" using Total_r
        unfolding r'_def total_on_def Field_def Domain_fst Range_snd image_def
        apply auto
        apply (metis (mono_tags, lifting) UnI1 fst_eqD mem_Collect_eq)
        apply (smt2 Un_def fst_conv mem_Collect_eq snd_conv)
        apply (smt2 Un_def fst_conv mem_Collect_eq snd_conv)
        by (smt2 Un_iff mem_Collect_eq snd_conv)        
      have wf_r: "wf (r - Id)" using Wo_r unfolding well_order_on_def by simp
      have Linear_order_r: "Linear_order r" using Wo_r unfolding well_order_on_def by simp
      have Linear_order_r': "Linear_order r'"
        by (metis R_r' Total_r' antisym_r' linear_order_on_def 
            partial_order_on_def preorder_on_def trans_r')
      show "wf (r' - Id)"
        unfolding Linear_order_wf_diff_Id[OF Linear_order_r']
      proof clarify
        fix A assume A: "A ⊆ Field r'" and A_not_empty: "A ≠ {}"
        def B == "f n ` A"
        have B: "B ⊆ Field r" using r'_subset_Yn A fn_Pi unfolding B_def Xn by auto
        have B_not_empty: "B ≠ {}" using A_not_empty unfolding B_def by auto            
        hence "∃a∈B. ∀a'∈B. (a, a') ∈ r" 
          using wf_r B B_not_empty unfolding Linear_order_wf_diff_Id[OF Linear_order_r] by simp
        from this obtain a where a: "a∈B" and all_Br: "∀a'∈B. (a, a') ∈ r" by auto            
        show "∃a∈A. ∀a'∈A. (a, a') ∈ r'"
        proof (rule bexI[of _ "g n a"])
          show "g n a ∈ A" (*by (metis B_def a comp_apply g2 id_apply image_iff)*)
            using g2 a unfolding compose_def restrict_def B_def
            by (auto, metis A DEADID.map_id contra_subsetD r'_subset_Yn)
          show "∀a'∈A. (g n a, a') ∈ r'" 
          proof
            fix a' assume a': "a' ∈ A" 
            have fna'_in_B: "(f n a') ∈ B" by (metis B_def a' image_eqI)
            have gn_fn_a': "a' = g n (f n a')"
              using g2 a' unfolding compose_def restrict_def
              by (metis A id_apply r'_subset_Yn subsetCE) 
            have "(a, f n a') ∈ r" using all_Br a fna'_in_B by auto
            thus "(g n a, a') ∈ r'" by (subst gn_fn_a', auto simp add: r'_def)
          qed
        qed
      qed 
    qed             
    have embed_g: "embed r r' (g n)"
    proof (unfold embed_iff_compat_inj_on_ofilter[OF Wo_r Wo_r'], auto)
      show "compat r r' (g n)" unfolding compat_def unfolding r'_def by auto
      show "inj_on (g n) (Field r)" 
        unfolding inj_on_def unfolding Xn proof auto
        fix x y assume x: "x ∈ X n" and y: "y ∈ X n" and gx_gy: "g n x = g n y"
        hence "f n (g n x) = f n (g n y)" by simp
        thus "x = y" using g2 unfolding compose_def restrict_def
          by (metis DEADID.map_id x y)
      qed
      show "ofilter r' (g n ` Field r)"
        unfolding ofilter_def under_def r'_def Field_def by (auto, auto simp add: Domain_fst)
    qed
    show "∃r'. Well_order r' ∧ Field r' = Y n ∧ iso r r' (g n)"
    proof (rule exI[of _ r'], auto simp add: Wo_r' )
      fix y assume "y ∈ Field r'" thus "y ∈ Y n" using r'_subset_Yn by auto
    next
      fix y assume y: "y ∈ Y n" 
      have fny: "f n y ∈ X n" 
        using s y 
        unfolding morphism_def simplicial_set_iso_def simplicial_set_wo_iso_def Func_def by auto
      have y_gf: "y = g n (f n y)"
        using g2 y unfolding compose_def restrict_def
        by (metis DEADID.map_id y)
      show "y ∈ Field r'"
      proof (subst y_gf, rule embed_in_Field[OF Wo_r])
        show "f n y ∈ Field r" using fny unfolding Xn .
        show "embed r r' (g n)" using embed_g .
      qed
    next
      show "iso r r' (g n)" 
        by (unfold iso_iff[OF Wo_r], simp add: embed_g, 
          auto simp add: r'_def Field_def, auto simp add: Domain_fst)
    qed 
  qed 
qed

end

subsection{*Isomorphism between well-ordered morphisms*}

context three_simplicial_sets
begin

text{*This is the definition of isomorphims between well-ordered morphisms that Voevodsky presents in his paper.*}

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 ∈ Y1 n. (fst(f2) n) (g n y) = (fst(f1) n) y) (*Commute*)
  ∧ (∀n::nat. ∀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

text{*
  We prove it thanks we have proven something more general 
  @{thm "iso_between_morphism_weak_unique"[no_vars]}, where we just demand morphism and not 
  isomorphism between simplicial sets.
  *}


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 simp


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_def
      by simp
    moreover have "f n a = undefined"
      using f False
      unfolding iso_between_morphism_def simplicial_set_iso_def morphism_def Func_def
      by simp
    ultimately show ?thesis ..
  qed
qed
end


context three_simplicial_sets
begin

lemma Field_ord1:
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Field (ord1 n x) = {y. y ∈ Y1 n ∧ f1 n y = x}"
  using f unfolding iso_between_morphism_def 
  unfolding Y1_X.well_ordered_morphism_def snd_conv 
  by (smt2 Collect_cong Pi_split_insert_domain x fst_conv mem_Collect_eq 
    mk_disjoint_insert well_order_on_Field)

lemma Field_ord2:
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Field (ord2 n x) = {y. y ∈ Y2 n ∧ f2 n y = x}"
  using f unfolding iso_between_morphism_def 
  unfolding Y2_X.well_ordered_morphism_def snd_conv 
  by (smt2 Collect_cong Pi_split_insert_domain `x ∈ X n` fst_conv mem_Collect_eq 
    mk_disjoint_insert well_order_on_Field)

lemma Field_ord1_in_Y1: 
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Field (ord1 n x) ⊆ Y1 n" by (metis Collect_restrict Field_ord1[OF x f])


lemma Field_ord2_in_Y2: 
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Field (ord2 n x) ⊆ Y2 n" by (metis Collect_restrict Field_ord2[OF x f])

lemma well_order_on_ord1: 
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "well_order_on {y ∈ Y1 n. f1 n y = x} (ord1 n x)" 
  using f unfolding iso_between_morphism_def 
  unfolding Y1_X.well_ordered_morphism_def
  unfolding Let_def fst_conv snd_conv using x by auto

lemma well_order_on_ord2: 
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "well_order_on {y ∈ Y2 n. f2 n y = x} (ord2 n x)" 
  using f unfolding iso_between_morphism_def 
  unfolding Y2_X.well_ordered_morphism_def
  unfolding Let_def fst_conv snd_conv using x by auto


lemma Well_order_ord1:
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Well_order (ord1 n x)" 
  using well_order_on_ord1[OF x f] 
  unfolding Field_ord1[OF x f, symmetric] .


lemma Well_order_ord2:
  assumes x: "x ∈ X n" and f: "iso_between_morphism (f1,ord1) (f2,ord2) f"
  shows "Well_order (ord2 n x)" 
  using well_order_on_ord2[OF x f] 
  unfolding Field_ord2[OF x f, symmetric] .


end

subsection{*The quotient set $W$*}

context simplicial_set
begin

(*
  definition "W3 = {f. ∃(Y::nat=>'b set) \<dd>y sy.  two_simplicial_sets.morphism Y \<dd>y sy X \<dd> s f}"
*)

(*
  definition "W2 α = {f. ∃(Y::nat=>'b set) \<dd>y sy. two_simplicial_sets.morphism Y \<dd>y sy X \<dd> s f
  ∧ two_simplicial_sets.α_small Y \<dd>y sy X \<dd> s α f}"
*)

definition "W2 = {f. ∃(Y::nat=>'b set) \<dd>y sy. two_simplicial_sets.morphism Y \<dd>y sy X \<dd> s f}"

(*
  lemma W2_in_W3: "(W2 α) ⊆ W3" unfolding W3_def W2_def by auto
*)


(*We are in a context where X is fixed as a simplicial set. If we write the following we are NOT
  stating that Y is another simplicial set:

  two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f,ord)*)

(*
  definition "W1 α = {(f,ord). ∃(Y::nat=>'b set) \<dd>y sy. class.simplicial_set Y \<dd>y sy 
  ∧ two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f,ord)
  ∧ two_simplicial_sets.α_small Y \<dd>y sy X \<dd> s α f}"
*)

definition "W1 = {(f,ord). ∃(Y::nat=>'b set) \<dd>y sy. class.simplicial_set Y \<dd>y sy 
  ∧ two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f,ord)}"


lemma W1_in_W3: "fst` (W1) ⊆ W2" unfolding W1_def W2_def
proof (auto simp add: two_simplicial_sets.well_ordered_morphism_def)
  fix a b Y \<dd>y sy
  assume 1: "two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (a, b)" 
    and 2: "class.simplicial_set Y \<dd>y sy"
  show "∃Y \<dd>y sy. two_simplicial_sets.morphism Y \<dd>y sy X \<dd> s a"
  proof (rule exI[of _ Y], rule exI[of _ \<dd>y], rule exI[of _ sy])
    interpret Y_X: two_simplicial_sets Y \<dd>y sy X \<dd> s using 2 unfolding class.simplicial_set_def
      by (unfold_locales, auto)
    show "two_simplicial_sets.morphism Y \<dd>y sy X \<dd> s a" 
      using 1 unfolding Y_X.well_ordered_morphism_def Let_def fst_conv by auto
  qed
qed


  (*
    In the following definition, f1 and f2 are of different types, 
    so Y1 Y2 X all of them are of different type as well.
  *)

definition "rel = {((f1,ord1),(f2,ord2)). ∃ Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 g. 
  class.simplicial_set Y1 \<dd>y1 sy1 ∧
  class.simplicial_set Y2 \<dd>y2 sy2 ∧
  three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1,ord1) (f2,ord2) g}"


lemma refl_on_W1_rel: "refl_on W1 rel"
proof (unfold refl_on_def rel_def, auto)
  fix Y1::"nat => 'b set" and Y2::"nat => 'd set" and a b aa ba \<dd>y1 sy1 \<dd>y2 sy2 x
  assume ss_Y1: "class.simplicial_set (Y1) \<dd>y1 sy1"
    and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2" 
    and i: "three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (a, b) (aa, ba) x "
  interpret X_Y1_Y2: three_simplicial_sets X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2
  using ss_Y1 ss_Y2 by (intro_locales, simp+)
  interpret Y2_X: two_simplicial_sets Y2 \<dd>y2 sy2 X \<dd> s using ss_Y1 ss_Y2 by (intro_locales)
  show "(a, b) ∈ W1" 
    unfolding W1_def using i ss_Y1 unfolding X_Y1_Y2.iso_between_morphism_def 
    unfolding X_Y1_Y2.Y2_X.well_ordered_morphism_def by auto
  show "(aa, ba) ∈ W1" unfolding W1_def
    apply (auto, rule exI[of _ Y2], rule exI[of _ \<dd>y2],rule exI[of _ sy2])       
    using i ss_Y2 unfolding X_Y1_Y2.iso_between_morphism_def
    unfolding X_Y1_Y2.Y2_X.well_ordered_morphism_def by auto
next
  fix f::"nat => 'b => 'a" 
    and ord 
  assume ab: "(f, ord) ∈ W1"
  from this obtain Y::"nat=>'b set" and \<dd>y sy where ss_Y: "class.simplicial_set Y \<dd>y sy"
    and wom: "two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f, ord)" unfolding W1_def by auto
  interpret Y_X: two_simplicial_sets Y \<dd>y sy X \<dd> s using ss_Y by (intro_locales, simp)
  interpret Y_Y: two_simplicial_sets Y \<dd>y sy Y \<dd>y sy  by intro_locales
  interpret X_Y_Y: three_simplicial_sets X \<dd> s Y \<dd>y sy Y \<dd>y sy  using ss_Y by intro_locales
  have iso_f: "X_Y_Y.iso_between_morphism (f, ord) (f, ord) (λn.λx∈Y n. x)" (*Maybe this should be an auxiliar lemma*)
    unfolding X_Y_Y.iso_between_morphism_def 
    apply (auto simp add: wom Y_Y.simplicial_set_iso_def Y_Y.morphism_def Func_def)
    apply (metis (full_types) Suc_eq_plus1 Y_X.\<dd>_pi funcset_mem)
    apply (metis Suc_eq_plus1 Y_X.s_pi funcset_mem)
    apply (rule exI[of _ "λn. λx∈Y n. x"], auto simp add: o_def)
    apply (metis (full_types) Suc_eq_plus1 Y_X.\<dd>_pi funcset_mem)
    apply (metis Suc_eq_plus1 Y_X.s_pi funcset_mem)
    apply (auto simp add: compose_def restrict_def)
  proof -
    fix n x assume x: "x∈X n"
    have field_ord: "Field (ord n x) ⊆ Y n"
    proof -
      have "Field (ord n x) = {y. y ∈ Y n ∧ f n y = x}"
        using wom unfolding Y_X.well_ordered_morphism_def snd_conv 
        by (smt2 Collect_cong Pi_split_insert_domain x fst_conv mem_Collect_eq 
          mk_disjoint_insert well_order_on_Field)
      thus ?thesis by auto
    qed
    have "iso (ord n x) (ord n x) (λx. if x ∈ Y n then x else undefined) = iso (ord n x) (ord n x) id"
    proof (rule iso_cong) 
      fix a assume a: "a ∈ Field (ord n x)"
      thus "(if a ∈ Y n then a else undefined) = id a" using field_ord by auto    
    qed
    thus "iso (ord n x) (ord n x) (λx. if x ∈ Y n then x else undefined)" using id_iso by auto
  qed
  show "∃Y1 \<dd>y1 sy1. class.simplicial_set Y1 \<dd>y1 sy1 ∧
    (∃Y2 \<dd>y2 sy2. class.simplicial_set Y2 \<dd>y2 sy2 
    ∧ Ex (three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f, ord) (f, ord)))"
    using iso_f ss_Y by fast
qed


lemma sym_rel: "sym rel"
proof (unfold sym_def rel_def, auto)
  fix Y1::"nat => 'b set" and Y2::"nat => 'd set" and f1 ord1 f2 ord2 \<dd>y1 sy1 \<dd>y2 sy2 f
  assume ss_Y1: "class.simplicial_set Y1 \<dd>y1 sy1"
    and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2" 
    and i: "three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1, ord1) (f2, ord2) f"
  interpret Y2_Y1: two_simplicial_sets Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 using ss_Y1 ss_Y2 by intro_locales
  interpret Y1_X: two_simplicial_sets Y1 \<dd>y1 sy1 X \<dd> s using ss_Y1 by intro_locales
  interpret Y2_X: two_simplicial_sets Y2 \<dd>y2 sy2 X \<dd> s using ss_Y1 by intro_locales
  interpret X_Y2_Y1: three_simplicial_sets X \<dd> s Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 using ss_Y1 ss_Y2 by intro_locales
  interpret X_Y1_Y2: three_simplicial_sets X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 using ss_Y1 ss_Y2 by intro_locales
  have f: "X_Y1_Y2.iso_between_morphism (f1, ord1) (f2, ord2) f" using i by simp
  obtain g where ssiso_g: "Y2_Y1.simplicial_set_iso g"
    and g2: "(∀n. compose (Y2 n) (f n) (g n) = restrict id (Y2 n) 
    ∧ compose (Y1 n) (g n) (f n) = restrict id (Y1 n))"
    using i unfolding X_Y1_Y2.iso_between_morphism_def 
    by (metis Y2_Y1.X_Y.simplicial_set_iso_g) 
  have ibm_g:"X_Y2_Y1.iso_between_morphism (f2, ord2) (f1, ord1) g"
  proof -
    have commute_f: "(∀n. ∀y∈Y1 n. f2 n (f n y) = f1 n y)" 
      using i ssiso_g unfolding X_Y1_Y2.iso_between_morphism_def
      unfolding X_Y2_Y1.iso_between_morphism_def o_def fst_conv by auto
    have iso_f: "(∀n. ∀x∈X n. iso (ord1 n x) (ord2 n x) (f n))"
      using f unfolding X_Y1_Y2.iso_between_morphism_def 
      unfolding Y1_X.well_ordered_morphism_def snd_conv by simp
    have "(∀n. ∀y∈Y2 n. f1 n (g n y) = f2 n y)"
    proof (rule+)
      fix n y
      assume y: "y ∈ Y2 n"
      have ssiso_f: "Y2_Y1.X_Y.simplicial_set_iso f" 
        using f unfolding X_Y1_Y2.iso_between_morphism_def by auto
      obtain x where y_fnx: "y = f n x" and x: "x ∈ Y1 n" 
        using y Y2_Y1.X_Y.simplicial_set_iso_bij[OF ssiso_f, of n]
        unfolding bij_betw_def image_def by auto
      have gn_fn_x: "(g n (f n x)) = x" using g2 unfolding compose_def
        by (metis DEADID.map_id restrict_def x) 
      have "f1 n (g n y) = f1 n (g n (f n x))" unfolding y_fnx ..
      also have "... = f1 n x" unfolding gn_fn_x ..
      also have "... = f2 n (f n x)" using commute_f x by auto
      also have "... = f2 n y" unfolding y_fnx ..
      finally show "f1 n (g n y) = f2 n y" .
    qed
    moreover have "(∀n. ∀x∈X n. iso (snd (f2, ord2) n x) (snd (f1, ord1) n x) (g n))"
    proof (unfold iso_def snd_conv, auto)        
      fix n x assume x: "x ∈ X n"         
      have Field_ord1: "Field (ord1 n x) = {y. y ∈ Y1 n ∧ f1 n y = x}"
        using f using X_Y1_Y2.Field_ord1 x by auto
      have Field_ord2: "Field (ord2 n x) = {y ∈ Y2 n. f2 n y = x}"
        using f using X_Y1_Y2.Field_ord2 x by auto
      have Wo_1: "Well_order (ord1 n x)"using f using X_Y1_Y2.Well_order_ord1 x by auto
      have Wo_2: "Well_order (ord2 n x)" using f using X_Y1_Y2.Well_order_ord2 x by auto      
      have gn_eq: "g n = (λy. if y ∈ (Field (ord2 n x)) then (inv_into (Field (ord1 n x)) (f n)) y else g n y)"
        unfolding inv_into_def 
      proof (rule, rule someI, auto)
        fix y assume y: "y ∈ Field (ord2 n x)"
        hence y2: "x = f2 n y" unfolding Field_ord2 by auto
        have y3: "y∈ Y2 n" using Field_ord2 y by blast
        show "g n y = (SOME ya. ya ∈ Field (ord1 n x) ∧ f n ya = y)" 
        proof (rule someI2_ex, rule exI[of _ "g n y"], auto simp add: Field_ord1)
          show gny_Y1: "g n y ∈ Y1 n" 
            by (metis (erased, hide_lams) X_Y1_Y2.Field_ord2_in_Y2[OF x f] 
              bij_betw_def contra_subsetD 
              image_eqI local.Y2_Y1.simplicial_set_iso_bij ssiso_g y)
          show fn_gn_y: "f n (g n y) = y" using g2 unfolding compose_def restrict_def 
            by (metis id_def y3) 
          show "f1 n (g n y) = x" by (metis fn_gn_y gny_Y1 commute_f y2)
          show "!!ya. ya ∈ Y1 n ==> x = f1 n ya ==> y = f n ya ==> g n (f n ya) = ya"
            using g2 unfolding compose_def restrict_def id_def by meson
        qed 
      qed
      have "embed (ord2 n x) (ord1 n x) (inv_into (Field (ord1 n x)) (f n))" 
        by (metis Wo_1 `x ∈ X n` iso_def iso_f iso_inv_into)
      thus "embed (ord2 n x) (ord1 n x) (g n)"
        by (metis (mono_tags, hide_lams) gn_eq embed_cong)
      thus "bij_betw (g n) (Field (ord2 n x)) (Field (ord1 n x))" 
        by (metis Wo_1 Wo_2 x embed_bothWays_bij_betw iso_def iso_f)
    qed
    ultimately show ?thesis 
      using i ssiso_g unfolding X_Y1_Y2.iso_between_morphism_def
      unfolding X_Y2_Y1.iso_between_morphism_def o_def by auto
  qed
  thus "∃Y1 \<dd>y1 sy1. class.simplicial_set Y1 \<dd>y1 sy1 ∧ (∃Y2 \<dd>y2 sy2. class.simplicial_set Y2 \<dd>y2 sy2
    ∧ Ex (three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f2, ord2) (f1, ord1)))"
    using ss_Y1 ss_Y2 by fast
qed

  (*ESTO NO SE PUEDE DEMOSTRAR AL MENOS FACILMENTE.
    However, now we cannot prove the following lemma. 5 simplicial sets appear  (Y1, Y2, Y3, Y4, X)
    and it is known there exists an isomorphism:
    f: Y1 --> Y2 
    X

    And other:
    g: Y3 --> Y4
    X

    We know that both Y2 and Y3 have the same type and share the f2 which goes to X. I should demonstrate
    that Y2 and Y3 are equal, which seems not to be possible.

    SOLUTION: new definition, explicitly saying the source simplicial set of the morphism in the relation.
  *)

lemma "trans rel"
proof (unfold trans_def rel_def, clarify)
  oops

definition "W1' = {((f,ord),(Y,\<dd>y,sy)). class.simplicial_set Y \<dd>y sy 
  ∧ two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f,ord)}"

definition "rel2 = {(((f1,ord1),(Y1,\<dd>y1,sy1)),((f2,ord2),(Y2,\<dd>y2,sy2))). 
  class.simplicial_set Y1 \<dd>y1 sy1 ∧
  class.simplicial_set Y2 \<dd>y2 sy2 ∧ (∃g. 
  three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1,ord1) (f2,ord2) g)}"

end

  (*Composition of morphisms is a morphisms*)
lemma morphism_composition:
  assumes ss_Y1:"class.simplicial_set Y1 \<dd>y1 sy1" 
  and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2"
  and ss_Y3: "class.simplicial_set Y3 \<dd>y3 sy3 "
  and f: "two_simplicial_sets.morphism Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 f "
  and g: "two_simplicial_sets.morphism Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 g"
(*shows "two_simplicial_sets.morphism Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 (λn x. g n (f n x))" *)
  shows "two_simplicial_sets.morphism Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 (λn. compose (Y1 n) (g n) (f n))"
proof -
  interpret Y1_Y3: two_simplicial_sets Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 using ss_Y1 ss_Y3 by intro_locales
  interpret Y1_Y2: two_simplicial_sets Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 using ss_Y2 by intro_locales
  interpret Y2_Y3: two_simplicial_sets Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 by intro_locales
  have Pi_fn: "∀n. f n ∈ Y1 n -> Y2 n"
    using f
    unfolding Y1_Y2.simplicial_set_iso_def
    unfolding Y1_Y2.morphism_def Func_def by simp
  have Pi_gn: "∀n. g n ∈ Y2 n -> Y3 n"
    using g
    unfolding Y2_Y3.simplicial_set_iso_def
    unfolding Y2_Y3.morphism_def Func_def by simp
  show ?thesis 
    unfolding Y1_Y3.morphism_def o_def Func_def compose_def
  proof auto
    fix n x assume "x ∈ Y1 n" thus "g n (f n x) ∈ Y3 n" using Pi_fn Pi_gn by auto
  next
    fix n i x assume i_le_n: "i ≤ Suc n" and x: "x ∈ Y1 (Suc n)"
    thus "g n (f n (\<dd>y1 (Suc n) i x)) = \<dd>y3 (Suc n) i (g (Suc n) (f (Suc n) x))"
      using g f 
      unfolding Y1_Y2.morphism_def
      unfolding Y2_Y3.morphism_def
      by (auto, metis Pi_fn funcset_mem)
  next
    fix n i x assume i_le_n: "i ≤ n" and x: "x ∈ Y1 n"
    thus "g (Suc n) (f (Suc n) (sy1 n i x)) = sy3 n i (g n (f n x))"
      using g f 
      unfolding Y1_Y2.morphism_def
      unfolding Y2_Y3.morphism_def 
      by (auto, metis Pi_fn funcset_mem)
  next
    fix n i x assume "\<dd>y1 (Suc n) i x ∉ Y1 n"
      and "i ≤ Suc n" and "x ∈ Y1 (Suc n)"
    thus "undefined = \<dd>y3 (Suc n) i (g (Suc n) (f (Suc n) x))"
      by (metis Pi_iff Suc_eq_plus1 Y1_Y3.Y.\<dd>_pi)
  next
    fix n i x
    assume "sy1 n i x ∉ Y1 (Suc n)" and "i ≤ n" and "x ∈ Y1 n"
    thus "undefined = sy3 n i (g n (f n x))"
      by (metis Pi_iff Suc_eq_plus1 Y1_Y3.Y.s_pi)      
  qed
qed


lemma simplicial_set_iso_composition:
  assumes ss_Y1:"class.simplicial_set Y1 \<dd>y1 sy1" 
  and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2"
  and ss_Y3: "class.simplicial_set Y3 \<dd>y3 sy3 "
  and f: "two_simplicial_sets.simplicial_set_iso Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 f "
  and g: "two_simplicial_sets.simplicial_set_iso Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 g"
(*shows "two_simplicial_sets.simplicial_set_iso Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 (λn x. g n (f n x))" *)
  shows "two_simplicial_sets.simplicial_set_iso Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 (λn. compose (Y1 n) (g n) (f n))"
proof -
  interpret Y1_Y3: two_simplicial_sets Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 using ss_Y1 ss_Y3 by intro_locales
  interpret Y1_Y2: two_simplicial_sets Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 using ss_Y2 by intro_locales
  interpret Y2_Y3: two_simplicial_sets Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 by intro_locales
  obtain inv_g where inv_g: "Y2_Y3.X_Y.simplicial_set_iso inv_g"
    and inv_g2: "(∀n. compose (Y3 n) (g n) (inv_g n) = restrict id (Y3 n) 
    ∧ compose (Y2 n) (inv_g n) (g n) = restrict id (Y2 n))"
    using g 
    by (metis Y2_Y3.simplicial_set_iso_g)
  obtain inv_f where inv_f: "Y1_Y2.X_Y.simplicial_set_iso inv_f"
    and inv_f2: "(∀n. compose (Y2 n) (f n) (inv_f n) = restrict id (Y2 n) 
    ∧ compose (Y1 n) (inv_f n) (f n) = restrict id (Y1 n))"
    using f 
    by (metis Y1_Y2.simplicial_set_iso_g)
  have Pi_fn: "∀n. f n ∈ Y1 n -> Y2 n" 
    using f
    unfolding Y1_Y2.simplicial_set_iso_def
    unfolding Y1_Y2.morphism_def Func_def by simp
  have Pi_gn: "∀n. g n ∈ Y2 n -> Y3 n" 
    using g
    unfolding Y2_Y3.simplicial_set_iso_def
    unfolding Y2_Y3.morphism_def Func_def by simp
  have Pi_inv_gn: "∀n. inv_g n ∈ Y3 n -> Y2 n"
    using inv_g
    unfolding Y2_Y3.X_Y.simplicial_set_iso_def
    unfolding Y2_Y3.X_Y.morphism_def Func_def by auto
  have Pi_inv_fn: "∀n. inv_f n ∈ Y2 n -> Y1 n"
    using inv_f
    unfolding Y1_Y2.X_Y.simplicial_set_iso_def
    unfolding Y1_Y2.X_Y.morphism_def Func_def by auto
  show ?thesis 
    unfolding Y1_Y3.simplicial_set_iso_def Y1_Y3.morphism_def o_def Y1_Y3.X_Y.morphism_def
    unfolding Func_def compose_def
  proof auto
    fix n x assume "x ∈ Y1 n" thus "g n (f n x) ∈ Y3 n" using Pi_fn Pi_gn by auto
  next
    fix n i x assume i_le_n: "i ≤ Suc n" and "x ∈ Y1 (Suc n)"
    thus "g n (f n (\<dd>y1 (Suc n) i x)) = \<dd>y3 (Suc n) i (g (Suc n) (f (Suc n) x))"  
      using g f i_le_n
      unfolding Y1_Y2.simplicial_set_iso_def
      unfolding Y1_Y2.morphism_def
      unfolding Y2_Y3.simplicial_set_iso_def
      unfolding Y2_Y3.morphism_def
      by (auto, metis Pi_fn funcset_mem)
  next
    fix n i x assume i_le_n: "i ≤ n" and "x ∈ Y1 n"
    thus "g (Suc n) (f (Suc n) (sy1 n i x)) = sy3 n i (g n (f n x))"
      using g f i_le_n
      unfolding Y1_Y2.simplicial_set_iso_def
      unfolding Y1_Y2.morphism_def
      unfolding Y2_Y3.simplicial_set_iso_def
      unfolding Y2_Y3.morphism_def 
      by (auto, metis Pi_fn funcset_mem)
  next
    show "∃ga. (∀n. (∀a∈Y3 n. ga n a ∈ Y1 n) ∧
      (∀a. a ∉ Y3 n --> ga n a = undefined) ∧
      (∀i x. i ≤ Suc n ∧ x ∈ Y3 (Suc n) --> ga n (\<dd>y3 (Suc n) i x) = \<dd>y1 (Suc n) i (ga (Suc n) x)) ∧
      (∀i x. i ≤ n ∧ x ∈ Y3 n --> ga (Suc n) (sy3 n i x) = sy1 n i (ga n x))) ∧
      (∀n. (λx∈Y3 n. if ga n x ∈ Y1 n then g n (f n (ga n x)) else undefined) = restrict id (Y3 n) ∧
      (λx∈Y1 n. ga n (if x ∈ Y1 n then g n (f n x) else undefined)) = restrict id (Y1 n))"
    proof (rule exI[of _ "λn. compose (Y3 n) (inv_f n) (inv_g n)"], 
        auto simp add: compose_def restrict_def fun_eq_iff)
      fix n x assume x: "x ∈ Y3 n"
      thus "inv_f n (inv_g n x) ∈ Y1 n" using Pi_inv_fn Pi_inv_gn by auto
    next
      fix n i x assume i_le_n: "i ≤ Suc n" and "x ∈ Y3 (Suc n)"
      thus "inv_f n (inv_g n (\<dd>y3 (Suc n) i x)) = \<dd>y1 (Suc n) i (inv_f (Suc n) (inv_g (Suc n) x))"
        using inv_g inv_f i_le_n inv_g2 inv_f2
        unfolding Y1_Y2.X_Y.simplicial_set_iso_def
        unfolding Y1_Y2.X_Y.morphism_def
        unfolding Y2_Y3.X_Y.simplicial_set_iso_def
        unfolding Y2_Y3.X_Y.morphism_def
        by (auto, metis Func_elim)
    next
      fix n i x assume i_le_n: "i ≤ n" and "x ∈ Y3 n"
      thus "inv_f (Suc n) (inv_g (Suc n) (sy3 n i x)) = sy1 n i (inv_f n (inv_g n x))"
        using inv_g inv_f i_le_n inv_g2 inv_f2
        unfolding Y1_Y2.X_Y.simplicial_set_iso_def
        unfolding Y1_Y2.X_Y.morphism_def
        unfolding Y2_Y3.X_Y.simplicial_set_iso_def
        unfolding Y2_Y3.X_Y.morphism_def 
        by (auto, metis Func_elim)
    next
      fix n i x
      assume "\<dd>y3 (Suc n) i x ∉ Y3 n " and "i ≤ Suc n" and "x ∈ Y3 (Suc n)"
      thus "undefined = \<dd>y1 (Suc n) i (inv_f (Suc n) (inv_g (Suc n) x))"
        by (metis Suc_eq_plus1 Y1_Y3.X.\<dd>_pi funcset_mem)
    next
      fix n i x
      assume "sy3 n i x ∉ Y3 (Suc n)" and "i ≤ n" and "x ∈ Y3 n"
      thus "undefined = sy1 n i (inv_f n (inv_g n x))"
        by (metis PiE Suc_eq_plus1 Y1_Y3.X.s_pi)
    next
      fix n x
      fix x  assume "inv_f n (inv_g n x) ∈ Y1 n" and x: "x ∈ Y3 n"
      have "g n (f n (inv_f n (inv_g n x))) = g n (inv_g n x)" 
        using inv_f2 unfolding compose_def restrict_def
        by (metis DEADID.map_id Pi_inv_gn x funcset_mem)
      also have "... = x" using inv_g2 unfolding compose_def restrict_def
      by (metis DEADID.map_id x)
      finally show "g n (f n (inv_f n (inv_g n x))) = x" .
    next
      fix x n assume a: "inv_f n (inv_g n x) ∉ Y1 n" and x: "x ∈ Y3 n" 
      have "inv_f n (inv_g n x) ∈ Y1 n"  using Pi_inv_fn Pi_inv_gn x by auto
      thus "undefined = x" using a by contradiction
    next
      fix n x assume "g n (f n x) ∈ Y3 n" and x: "x ∈ Y1 n"
      have "inv_f n (inv_g n (g n (f n x))) = inv_f n (f n x)" 
        using inv_g2 unfolding compose_def restrict_def 
        by (metis DEADID.map_id Pi_fn funcset_mem x)
      also have "... = x" using inv_f2
        unfolding compose_def restrict_def by (metis DEADID.map_id x)
      finally show "inv_f n (inv_g n (g n (f n x))) = x" .
    next
      fix n x assume gn_fn_Y3: "g n (f n x) ∉ Y3 n" and x: "x ∈ Y1 n"
      have "g n (f n x) ∈ Y3 n" by (metis Pi_fn Pi_gn Pi_iff x) 
      thus "undefined = x" using gn_fn_Y3 by contradiction
    qed
    fix n i x
    assume "\<dd>y1 (Suc n) i x ∉ Y1 n" and "i ≤ Suc n" and "x ∈ Y1 (Suc n)"
    thus "undefined = \<dd>y3 (Suc n) i (g (Suc n) (f (Suc n) x))" 
      by (metis Suc_eq_plus1 Y1_Y3.Y.\<dd>_pi funcset_mem)
  next
    fix n i x
    assume "sy1 n i x ∉ Y1 (Suc n)" and "i ≤ n" and "x ∈ Y1 n"
    thus "undefined = sy3 n i (g n (f n x))"
      by (metis PiE Suc_eq_plus1 Y1_Y3.Y.s_pi)
  qed
qed

(*
    Important: trans, sym and refl demand the related elements to be of the same type, which means
    that Y1 and Y2 must be of the same type.
*)

(*
    I try to explicitly prove the property of transitivity without the predicate trans. Hence, we will
    be able to prove the property involving more general types ('a, 'b and 'c, not only 'a).
    In order to do that, I have to define a locale where 4 simplicial sets are fixed.
*)

locale four_simplicial_sets = X: simplicial_set X \<dd>x sx 
  + Y1: simplicial_set Y1 \<dd>y1 sy1 + Y2: simplicial_set Y2 \<dd>y2 sy2  
  + Y3: simplicial_set Y3 \<dd>y3 sy3 
  for X::"nat => 'a set" 
  and \<dd>x :: "nat => nat => 'a => 'a"
  and sx :: "nat => nat => 'a => 'a"
  and Y1::"nat => 'b set" 
  and \<dd>y1 :: "nat => nat => 'b => 'b"
  and sy1 :: "nat => nat => 'b => 'b"
  and Y2 :: "nat => 'c set" 
  and \<dd>y2 :: "nat => nat => 'c => 'c"
  and sy2 :: "nat => nat => 'c => 'c"
  and Y3 :: "nat => 'd set" 
  and \<dd>y3 :: "nat => nat => 'd => 'd"
  and sy3 :: "nat => nat => 'd => 'd" 
begin

sublocale X_Y1_Y2: three_simplicial_sets X \<dd>x sx Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 by unfold_locales
sublocale X_Y2_Y3: three_simplicial_sets X \<dd>x sx Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 by unfold_locales
sublocale X_Y1_Y3: three_simplicial_sets X \<dd>x sx Y1 \<dd>y1 sy1 Y3 \<dd>y3 sy3 by unfold_locales

lemma trans_extended:
  assumes f: "X_Y1_Y2.iso_between_morphism (f1,ord1) (f2,ord2) f"
  and g: "X_Y2_Y3.iso_between_morphism (f2,ord2) (f3,ord3) g"
  shows "∃h. X_Y1_Y3.iso_between_morphism (f1,ord1) (f3,ord3) h"
proof -
  have ss_Y1: "class.simplicial_set Y1 \<dd>y1 sy1" by unfold_locales
  have ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2" by unfold_locales
  have ss_Y3: "class.simplicial_set Y3 \<dd>y3 sy3" by unfold_locales
  obtain inv_g where inv_g: "X_Y2_Y3.Y1_Y2.X_Y.simplicial_set_iso inv_g"
    and inv_g2: "(∀n. compose (Y3 n) (g n) (inv_g n) = restrict id (Y3 n) 
    ∧ compose (Y2 n) (inv_g n) (g n) = restrict id (Y2 n))"
    using g unfolding X_Y2_Y3.iso_between_morphism_def 
    by (metis X_Y2_Y3.Y1_Y2.simplicial_set_iso_g)
  obtain inv_f where inv_f: "X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso inv_f"
    and inv_f2: "(∀n. compose (Y2 n) (f n) (inv_f n) = restrict id (Y2 n) 
    ∧ compose (Y1 n) (inv_f n) (f n) = restrict id (Y1 n))"
    using f unfolding X_Y1_Y2.iso_between_morphism_def 
    by (metis X_Y1_Y2.Y1_Y2.simplicial_set_iso_g)
  have Pi_fn: "∀n. f n ∈ Y1 n -> Y2 n"
    using f
    unfolding X_Y1_Y2.iso_between_morphism_def X_Y1_Y2.Y1_Y2.simplicial_set_iso_def
    unfolding X_Y1_Y2.Y1_Y2.morphism_def Func_def by simp
  have Pi_gn: "∀n. g n ∈ Y2 n -> Y3 n"
    using g
    unfolding X_Y2_Y3.iso_between_morphism_def X_Y2_Y3.Y1_Y2.simplicial_set_iso_def
    unfolding X_Y2_Y3.Y1_Y2.morphism_def Func_def by simp
  have Pi_inv_gn: "∀n. inv_g n ∈ Y3 n -> Y2 n"
    using inv_g
    unfolding X_Y2_Y3.iso_between_morphism_def X_Y2_Y3.Y1_Y2.X_Y.simplicial_set_iso_def
    unfolding X_Y2_Y3.Y1_Y2.X_Y.morphism_def Func_def by simp
  have Pi_inv_fn: "∀n. inv_f n ∈ Y2 n -> Y1 n"
    using inv_f
    unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def
    unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def Func_def by auto
  have "X_Y1_Y3.iso_between_morphism (f1, ord1) (f3, ord3) (λn. compose (Y1 n) (g n) (f n))"
  proof -
    have f3_g_f: "(∀n. ∀y∈Y1 n. f3 n (g n (f n y)) = f1 n y)"
    proof (auto)
      fix n y assume y: "y ∈ Y1 n"
      have fny: "f n y ∈ Y2 n" using y Pi_fn by auto
      have "f3 n (g n (f n y)) = f2 n (f n y)" 
        using g fny unfolding X_Y2_Y3.iso_between_morphism_def fst_conv by auto
      also have "... = f1 n y" 
        using f y unfolding X_Y1_Y2.iso_between_morphism_def fst_conv by auto
      finally show "f3 n (g n (f n y)) = f1 n y" .
    qed
    have "(∀n. ∀y∈Y1 n. f3 n (compose (Y1 n) (g n) (f n) y) = f1 n y)" by (metis compose_eq f3_g_f)
    moreover have "X_Y1_Y3.Y1_Y2.simplicial_set_iso (λn. compose (Y1 n) (g n) (f n))" 
      using simplicial_set_iso_composition[OF ss_Y1 ss_Y2 ss_Y3]
      using f g
      unfolding X_Y1_Y2.iso_between_morphism_def 
      unfolding X_Y2_Y3.iso_between_morphism_def by auto
    moreover have "(∀n. ∀x∈X n. iso (ord1 n x) (ord3 n x) (compose (Y1 n) (g n) (f n)))"
    proof (auto)
      fix n x assume x: "x ∈ X n" 
      (*Some proofs here are similar to the one presented in the proof about symmetric relation.*)
      have Field_ord1: "Field (ord1 n x) = {y. y ∈ Y1 n ∧ f1 n y = x}"
        using f using X_Y1_Y2.Field_ord1 x by auto
      have Field_ord2: "Field (ord2 n x) = {y ∈ Y2 n. f2 n y = x}"
        using f using X_Y1_Y2.Field_ord2 x by auto
      have Field_ord2_in_Y2: "Field (ord2 n x) ⊆ Y2 n" by (metis Collect_restrict Field_ord2)
      have "well_order_on {y ∈ Y2 n. f2 n y = x} (ord2 n x)" 
        using f unfolding X_Y1_Y2.iso_between_morphism_def 
        unfolding X_Y1_Y2.Y2_X.well_ordered_morphism_def
        unfolding Let_def fst_conv snd_conv using x by auto
      hence Wo_2: "Well_order (ord2 n x)" unfolding Field_ord2[symmetric] .
      have Field_ord3: "Field (ord3 n x) = {y ∈ Y3 n. f3 n y = x}"
        using g unfolding X_Y2_Y3.iso_between_morphism_def 
        unfolding X_Y2_Y3.Y2_X.well_ordered_morphism_def snd_conv 
        by (smt2 Collect_cong Pi_split_insert_domain `x ∈ X n` fst_conv mem_Collect_eq 
          mk_disjoint_insert well_order_on_Field)
      have Field_ord3_in_Y3: "Field (ord3 n x) ⊆ Y3 n" by (metis Collect_restrict Field_ord3)
      have "well_order_on {y ∈ Y3 n. f3 n y = x} (ord3 n x)" 
        using g unfolding X_Y2_Y3.iso_between_morphism_def 
        unfolding X_Y2_Y3.Y2_X.well_ordered_morphism_def
        unfolding Let_def fst_conv snd_conv using x by auto
      hence Wo_3: "Well_order (ord3 n x)" unfolding Field_ord3[symmetric] .
      have "well_order_on {y ∈ Y1 n. f1 n y = x} (ord1 n x)" 
        using f unfolding X_Y1_Y2.iso_between_morphism_def 
        unfolding Y1_X.well_ordered_morphism_def
        unfolding Let_def fst_conv snd_conv using x by auto
      hence Wo_1: "Well_order (ord1 n x)" unfolding Field_ord1[symmetric] .
      show "iso (ord1 n x) (ord3 n x) (compose (Y1 n) (g n) (f n))"
      proof (unfold iso_iff3[OF Wo_1 Wo_3] compat_def bij_betw_def 
          image_def Field_ord3 Field_ord1, auto)
        show "inj_on (compose (Y1 n) (g n) (f n)) {y ∈ Y1 n. f1 n y = x}"
          unfolding inj_on_def using inv_f2 inv_g2
          unfolding compose_def restrict_def 
          by (auto, metis (no_types, lifting) DEADID.map_id Pi_fn Pi_iff)
        fix xa assume xa: "xa ∈ Y1 n" and f1_n_xa: "x = f1 n xa"
        show "f3 n (compose (Y1 n) (g n) (f n) xa) = f1 n xa" 
          using xa Pi_gn Pi_fn f3_g_f unfolding compose_def by auto
      next
        fix xa assume xa: "xa ∈ Y3 n" and f3xa: "x = f3 n xa" 
        show "∃x. x ∈ Y1 n ∧ f1 n x = f3 n xa ∧ xa = compose (Y1 n) (g n) (f n) x"
        proof (rule exI[of _ "inv_f n (inv_g n xa)"], auto)
          show "inv_f n (inv_g n xa) ∈ Y1 n" 
            by (metis Pi_inv_fn Pi_inv_gn Pi_split_insert_domain mk_disjoint_insert xa)
          thus "f1 n (inv_f n (inv_g n xa)) = f3 n xa" using inv_f2 inv_g2 f3_g_f
            unfolding compose_def restrict_def
            by (metis (no_types, lifting) DEADID.map_id Pi_iff Pi_inv_fn Pi_inv_gn f3xa xa)
          show "xa = compose (Y1 n) (g n) (f n) (inv_f n (inv_g n xa))"
            using inv_f2 inv_g2 unfolding compose_def
            by (metis DEADID.map_id Pi_inv_gn `inv_f n (inv_g n xa) ∈ Y1 n` funcset_mem restrict_apply' xa) 
        qed
      next
        fix xa assume "xa ∈ Y1 n" and "x = f1 n xa" thus "compose (Y1 n) (g n) (f n) xa ∈ Y3 n"
          unfolding compose_def 
          by (auto, metis Pi_fn Pi_gn funcset_mem)           
      next
        fix a b assume ab_ord1: "(a, b) ∈ ord1 n x"
        have iso_ord1_ord2: "(∀n. ∀x∈X n. iso (ord1 n x) (ord2 n x) (f n))"
          using f x unfolding X_Y1_Y2.iso_between_morphism_def snd_conv by auto
        have iso_ord2_ord3: "(∀n. ∀x∈X n. iso (ord2 n x) (ord3 n x) (g n))"
          using g x unfolding X_Y2_Y3.iso_between_morphism_def snd_conv by auto
        have compat_ord1_ord2: "compat (ord1 n x) (ord2 n x) (f n)"
          using iso_ord1_ord2 x using iso_iff3[OF Wo_1 Wo_2] by auto           
        hence fna_fnb_ord2: "((f n a), (f n b)) ∈ ord2 n x"
          unfolding compat_def using ab_ord1 by auto
        have compat_ord2_ord3: "compat (ord2 n x) (ord3 n x) (g n)"
          using iso_ord2_ord3 x using iso_iff3[OF Wo_2 Wo_3] by auto
        thus "(compose (Y1 n) (g n) (f n) a, compose (Y1 n) (g n) (f n) b) ∈ ord3 n x"
          using x fna_fnb_ord2 unfolding compat_def
          by (metis (erased, lifting) `well_order_on {y ∈ Y1 n. f1 n y = x} (ord1 n x)` 
            ab_ord1 compose_eq mem_Collect_eq well_order_on_domain) 
      qed           
    qed
    ultimately show ?thesis 
      unfolding X_Y1_Y3.iso_between_morphism_def
      using f unfolding X_Y1_Y2.iso_between_morphism_def      
      using g unfolding X_Y2_Y3.iso_between_morphism_def by simp
  qed
  thus "Ex (X_Y1_Y3.iso_between_morphism (f1, ord1) (f3, ord3))" by blast
qed


end


context simplicial_set
begin

(*
  The transitivity is a corollary.
*)

lemma trans_rel2: "trans rel2"
proof (unfold trans_def rel2_def, clarify)
  fix f1 ord1 f2 ord2 f3 ord3 Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 f Y3 \<dd>y3 sy3 g
  assume ss_Y1:"class.simplicial_set Y1 \<dd>y1 sy1" and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2"
    and f: "three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1, ord1) (f2, ord2) f "
    and ss_Y3: "class.simplicial_set Y3 \<dd>y3 sy3 "
    and g: "three_simplicial_sets.iso_between_morphism X \<dd> s Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 (f2, ord2) (f3, ord3) g"
  interpret X_Y1_Y2_Y3: four_simplicial_sets X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 Y3 \<dd>y3 sy3 
    using ss_Y1 ss_Y2 ss_Y3 by intro_locales
  obtain h where h: "X_Y1_Y2_Y3.X_Y1_Y3.iso_between_morphism (f1, ord1) (f3, ord3) h"
    using X_Y1_Y2_Y3.trans_extended f g by blast
  thus "Ex (X_Y1_Y2_Y3.X_Y1_Y3.iso_between_morphism (f1, ord1) (f3, ord3))" by blast
qed


lemma refl_on_W1'_rel2: "refl_on W1' rel2"
proof (unfold refl_on_def rel2_def W1'_def, auto)
  fix Y1::"nat => 'b set" and Y2::"nat => 'd set" and f1 f2 ord1 ord2 \<dd>y1 sy1 \<dd>y2 sy2 x
  assume ss_Y1: "class.simplicial_set (Y1) \<dd>y1 sy1"
    and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2" 
    and i: "three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1, ord1) (f2, ord2) x "
  interpret Y1_X: two_simplicial_sets Y1 \<dd>y1 sy1 X \<dd> s using ss_Y1 by intro_locales
  interpret Y2_X: two_simplicial_sets Y2 \<dd>y2 sy2 X \<dd> s using ss_Y1 ss_Y2 by intro_locales
  interpret X_Y1_Y2: three_simplicial_sets X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 by intro_locales
  show "Y1_X.well_ordered_morphism (f1, ord1)" and "Y2_X.well_ordered_morphism (f2, ord2)"
    using i unfolding X_Y1_Y2.iso_between_morphism_def by auto
next
  fix Y::"nat => 'b set" and f ord \<dd>y sy
  assume ss_Y: "class.simplicial_set Y \<dd>y sy"
    and wom: "two_simplicial_sets.well_ordered_morphism Y \<dd>y sy X \<dd> s (f, ord)"  
  interpret Y_X: two_simplicial_sets Y \<dd>y sy X \<dd> s using ss_Y by (intro_locales, simp)
  interpret Y_Y: two_simplicial_sets Y \<dd>y sy Y \<dd>y sy  by intro_locales
  interpret X_Y_Y: three_simplicial_sets X \<dd> s Y \<dd>y sy Y \<dd>y sy  using ss_Y by intro_locales
  have iso_f: "X_Y_Y.iso_between_morphism (f, ord) (f, ord) (λn. λx∈ Y n. x)"
  proof (auto simp add: X_Y_Y.iso_between_morphism_def 
    wom Y_Y.simplicial_set_iso_def Y_Y.morphism_def Func_def)
    fix n i x
    assume \<dd>y: "\<dd>y (Suc n) i x ∉ Y n" and i: "i ≤ Suc n" and x: "x ∈ Y (Suc n)"
    have "\<dd>y (Suc n) i x ∈ Y n" using x i Y_X.Y.\<dd>_pi by auto
    thus "undefined = \<dd>y (Suc n) i x" using \<dd>y by contradiction
  next
    fix n i x assume s: "sy n i x ∉ Y (Suc n)" and "i ≤ n" and "x ∈ Y n"
    thus "undefined = sy n i x" using s Y_X.Y.s_pi by auto
  next
    show "∃g. (∀n. (∀a∈Y n. g n a ∈ Y n) ∧
      (∀a. a ∉ Y n --> g n a = undefined) ∧
      (∀i x. i ≤ Suc n ∧ x ∈ Y (Suc n) --> g n (\<dd>y (Suc n) i x) = \<dd>y (Suc n) i (g (Suc n) x)) ∧
      (∀i x. i ≤ n ∧ x ∈ Y n --> g (Suc n) (sy n i x) = sy n i (g n x))) ∧
      (∀n. compose (Y n) (λx∈Y n. x) (g n) = restrict id (Y n) ∧ compose (Y n) (g n) (λx∈Y n. x) = restrict id (Y n))"
    proof (rule  exI[of _ "λn. λx∈Y n. x"], auto simp add: compose_def restrict_def)
      (*This has been repited previously*)
      fix n i x
      assume \<dd>y: "\<dd>y (Suc n) i x ∉ Y n" and i: "i ≤ Suc n" and x: "x ∈ Y (Suc n)"
      have "\<dd>y (Suc n) i x ∈ Y n" using x i Y_X.Y.\<dd>_pi by auto
      thus "undefined = \<dd>y (Suc n) i x" using \<dd>y by contradiction
    next
      fix n i x assume s: "sy n i x ∉ Y (Suc n)" and "i ≤ n" and "x ∈ Y n"
      thus "undefined = sy n i x" using s Y_X.Y.s_pi by auto
    qed
  next
    (*This has been obtained from the proof of lemma refl_on_W1_rel*)
    fix n x assume x: "x∈X n"
    have field_ord: "Field (ord n x) ⊆ Y n"
    proof -
      have "Field (ord n x) = {y. y ∈ Y n ∧ f n y = x}"
        using wom unfolding Y_X.well_ordered_morphism_def snd_conv 
        by (smt2 Collect_cong Pi_split_insert_domain x fst_conv mem_Collect_eq 
          mk_disjoint_insert well_order_on_Field)
      thus ?thesis by auto
    qed
    have "iso (ord n x) (ord n x) (λx∈Y n. x) = iso (ord n x) (ord n x) id"
    proof (rule iso_cong) 
      fix a assume a: "a ∈ Field (ord n x)"
      thus "(λx∈Y n. x) a  = id a" using field_ord by auto    
    qed
    thus "iso (ord n x) (ord n x) (λx∈Y n. x)" using id_iso by auto
  qed
  show "Ex (X_Y_Y.iso_between_morphism (f, ord) (f, ord))"
    using iso_f ss_Y by fast
qed

end


context simplicial_set
begin

term W1' 
term rel2

(*
  This is the quotient set. Y1 and Y2 have different types in rel2 (as well as in W1'), 
  but when doing the quotient set they must be equal.
*)

definition "W = W1' // rel2"

end


context three_simplicial_sets
begin

interpretation X_Y2_Y1: three_simplicial_sets X \<dd>x sx Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 by unfold_locales

(*
  This is the symmetric property (explicitly stated) but with generalized types.
*)

lemma sym_extended:
  assumes f: "iso_between_morphism (f1,ord1) (f2, ord2) f" 
  shows "∃g. three_simplicial_sets.iso_between_morphism 
  X \<dd>x sx Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 (f2,ord2) (f1, ord1) g 
  ∧  (∀n. compose (Y2 n) (f n) (g n) = restrict id (Y2 n) 
  ∧ compose (Y1 n)(g n) (f n) = restrict id (Y1 n))" 
proof -
  obtain g where ssiso_g: "Y1_Y2.X_Y.simplicial_set_iso g"
    and g2: "(∀n. compose (Y2 n) (f n) (g n) = restrict id (Y2 n) 
    ∧ compose (Y1 n)(g n) (f n) = restrict id (Y1 n))"
    using f unfolding iso_between_morphism_def 
    by (metis Y1_Y2.simplicial_set_iso_g) 
  have ibm_g:"X_Y2_Y1.iso_between_morphism (f2, ord2) (f1, ord1) g"
  proof -
    have commute_f: "(∀n. ∀y∈Y1 n. f2 n (f n y) = f1 n y)" 
      using f ssiso_g unfolding iso_between_morphism_def
      unfolding X_Y2_Y1.iso_between_morphism_def o_def fst_conv by auto
    have iso_f: "(∀n. ∀x∈X n. iso (ord1 n x) (ord2 n x) (f n))"
      using f unfolding iso_between_morphism_def 
      unfolding Y1_X.well_ordered_morphism_def snd_conv by simp
    have "(∀n. ∀y∈Y2 n. f1 n (g n y) = f2 n y)"
    proof (rule+)
      fix n y
      assume y: "y ∈ Y2 n"
      have ssiso_f: "Y1_Y2.simplicial_set_iso f" 
        using f unfolding iso_between_morphism_def by auto
      obtain x where y_fnx: "y = f n x" and x: "x ∈ Y1 n" 
        using y Y1_Y2.simplicial_set_iso_bij[OF ssiso_f, of n]
        unfolding bij_betw_def image_def by auto
      have gn_fn_x: "(g n (f n x)) = x" using g2 unfolding compose_def 
        by (metis DEADID.map_id restrict_def x)
      have "f1 n (g n y) = f1 n (g n (f n x))" unfolding y_fnx ..
      also have "... = f1 n x" unfolding gn_fn_x ..
      also have "... = f2 n (f n x)" using commute_f x by auto
      also have "... = f2 n y" unfolding y_fnx ..
      finally show "f1 n (g n y) = f2 n y" .
    qed
    moreover have "(∀n. ∀x∈X n. iso (snd (f2, ord2) n x) (snd (f1, ord1) n x) (g n))"
    proof (unfold iso_def snd_conv, auto)        
      fix n x assume x: "x ∈ X n"         
      have Field_ord1: "Field (ord1 n x) = {y. y ∈ Y1 n ∧ f1 n y = x}"
        using f unfolding iso_between_morphism_def 
        unfolding Y1_X.well_ordered_morphism_def snd_conv  
        by (smt2 Collect_cong Pi_split_insert_domain `x ∈ X n` fst_conv mem_Collect_eq 
          mk_disjoint_insert well_order_on_Field)
      have Field_ord2: "Field (ord2 n x) = {y ∈ Y2 n. f2 n y = x}"
        using f unfolding iso_between_morphism_def 
        unfolding Y2_X.well_ordered_morphism_def snd_conv 
        by (smt2 Collect_cong Pi_split_insert_domain `x ∈ X n` fst_conv mem_Collect_eq 
          mk_disjoint_insert well_order_on_Field)
      have Field_ord2_in_Y2: "Field (ord2 n x) ⊆ Y2 n" by (metis Collect_restrict Field_ord2)
      have "well_order_on {y ∈ Y2 n. f2 n y = x} (ord2 n x)" 
        using f unfolding iso_between_morphism_def 
        unfolding Y2_X.well_ordered_morphism_def
        unfolding Let_def fst_conv snd_conv using x by auto
      hence Wo_2: "Well_order (ord2 n x)" unfolding Field_ord2[symmetric] .
      have "well_order_on {y ∈ Y1 n. f1 n y = x} (ord1 n x)" 
        using f unfolding iso_between_morphism_def 
        unfolding Y1_X.well_ordered_morphism_def
        unfolding Let_def fst_conv snd_conv using x by auto
      hence Wo_1: "Well_order (ord1 n x)" unfolding Field_ord1[symmetric] .
      have gn_eq: "g n = (λy. if y ∈ (Field (ord2 n x)) then (inv_into (Field (ord1 n x)) (f n)) y else g n y)"
        unfolding inv_into_def 
      proof (rule, rule someI, auto)
        fix y assume y: "y ∈ Field (ord2 n x)"
        hence y2: "x = f2 n y" unfolding Field_ord2 by auto
        show "g n y = (SOME ya. ya ∈ Field (ord1 n x) ∧ f n ya = y)" 
        proof (rule someI2_ex, rule exI[of _ "g n y"], auto simp add: Field_ord1)
          show gny_Y1: "g n y ∈ Y1 n" 
            by (metis (erased, hide_lams) Field_ord2_in_Y2 bij_betw_def contra_subsetD 
              image_eqI Y1_Y2.X_Y.simplicial_set_iso_bij ssiso_g y)
          show fn_gn_y: "f n (g n y) = y" using g2 unfolding compose_def restrict_def 
            by (metis DEADID.map_id Field_ord2_in_Y2 contra_subsetD y)
          show "f1 n (g n y) = x" by (metis fn_gn_y gny_Y1 commute_f y2)
          show "!!ya. ya ∈ Y1 n ==> x = f1 n ya ==> y = f n ya ==> g n (f n ya) = ya"
            using g2 unfolding compose_def restrict_def by (metis DEADID.map_id)
        qed 
      qed
      have "embed (ord2 n x) (ord1 n x) (inv_into (Field (ord1 n x)) (f n))" 
        by (metis Wo_1 `x ∈ X n` iso_def iso_f iso_inv_into)
      thus "embed (ord2 n x) (ord1 n x) (g n)"
        by (metis (mono_tags, hide_lams) gn_eq embed_cong)
      thus "bij_betw (g n) (Field (ord2 n x)) (Field (ord1 n x))" 
        by (metis Wo_1 Wo_2 x embed_bothWays_bij_betw iso_def iso_f)
    qed
    ultimately show ?thesis 
      using f ssiso_g unfolding iso_between_morphism_def
      unfolding X_Y2_Y1.iso_between_morphism_def o_def by auto
  qed
  thus ?thesis using g2 by auto
qed

end

context simplicial_set
begin


(*
  This is now a corollary. Since we have made use of the predicate sym, types must be equal.
  This is because if (f::a=>b, g::a'=>b') belongs to the relation, then (g::a'=>b', f:: a=>b) must
  belong to the same relation as well and thus a'=a y b'=b.
  Same has happenned with the reflexivity and transitivity.
*)

corollary sym_rel2: "sym rel2"
proof (unfold sym_def rel2_def, auto)
  fix Y1::"nat => 'b set" and Y2::"nat => 'd set" and f1 ord1 f2 ord2 \<dd>y1 sy1 \<dd>y2 sy2 f
  assume ss_Y1: "class.simplicial_set Y1 \<dd>y1 sy1"
    and ss_Y2: "class.simplicial_set Y2 \<dd>y2 sy2" 
    and i: "three_simplicial_sets.iso_between_morphism X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1, ord1) (f2, ord2) f"
  interpret X_Y2_Y1: three_simplicial_sets X \<dd> s Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 using ss_Y1 ss_Y2 by intro_locales
  interpret X_Y1_Y2: three_simplicial_sets X \<dd> s Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 using ss_Y1 ss_Y2 by intro_locales
  have f: "X_Y1_Y2.iso_between_morphism (f1, ord1) (f2, ord2) f" using i by simp
  show "Ex (X_Y2_Y1.iso_between_morphism (f2, ord2) (f1, ord1))" using X_Y1_Y2.sym_extended[OF f] by auto
qed


lemma equiv_W1'_rel2:
  shows "equiv W1' rel2"
  by (unfold equiv_def, auto simp add: sym_rel2 trans_rel2 refl_on_W1'_rel2)

end

subsection{*Pullback*}

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. (\<dd>y i n (fst x), \<dd>x i n (snd x))) "
  "(λi n x. (sy i n (fst x), sx i n (snd x)))"
proof (unfold class.simplicial_set_def, auto)
  fix i q a assume iq: "i ≤ Suc q" and a: "a ∈ Y (Suc q)"
  thus "\<dd>y (Suc q) i a ∈ Y q"  using Y.\<dd>_pi by auto
next
  fix i q b assume iq: "i ≤ Suc q" and b: "b ∈ X (Suc q)"
  thus "\<dd>x (Suc q) i b ∈ X q"  using X.\<dd>_pi by auto
next
  fix i q a assume iq: "i ≤ q" and a: "a ∈ Y q"
  show "sy q i a ∈ Y (Suc q)" 
    by (metis One_nat_def Y.s_pi a add_Suc_right funcset_mem 
      iq monoid_add_class.add.right_neutral)
next
  fix i q b assume iq: "i ≤ q" and b: "b ∈ X q"
  thus "b ∈ X q ==> sx q i b ∈ X (Suc q)" 
    by (metis Suc_eq_plus1 X.s_pi funcset_mem)
next
  fix q b assume "b ∈ X q" thus "b ∈ X q" by simp
next
  fix q i j a b
  assume "0 < q" and "i < j" and "j ≤ Suc q" and "a ∈ Y (Suc q)" and "b ∈ X (Suc q)"
  thus "\<dd>y q i (\<dd>y (Suc q) j a) = \<dd>y q (j - Suc 0) (\<dd>y (Suc q) i a)" 
    and "\<dd>x q i (\<dd>x (Suc q) j b) = \<dd>x q (j - Suc 0) (\<dd>x (Suc q) i b)"
    using Y.condition1 X.condition1 by auto
next
  fix i j q a b
  assume ij: "i ≤ j" and jq: "j ≤ q" and "a ∈ Y q" and "b ∈ X q"
  thus "sy (Suc q) i (sy q j a) = sy (Suc q) (Suc j) (sy q i a)"
    and "sx (Suc q) i (sx q j b) = sx (Suc q) (Suc j) (sx q i b)"
    using Y.condition2 X.condition2 ij jq
    by auto
next
  fix i j q a b
  assume ij: "i < j" and jq: "j ≤ q" and "a ∈ Y q" and "b ∈ X q"
  thus "\<dd>y (Suc q) i (sy q j a) = sy (q - Suc 0) (j - Suc 0) (\<dd>y q i a)"
    and "\<dd>x (Suc q) i (sx q j b) = sx (q - Suc 0) (j - Suc 0) (\<dd>x q i b)"
    using Y.condition3 X.condition3
    by auto
next
  fix j q a b assume jq: "j ≤ q"  and "a ∈ Y q" and "b ∈ X q"
  thus "\<dd>y (Suc q) (Suc j) (sy q j a) = a" 
    and "\<dd>x (Suc q) (Suc j) (sx q j b) = b"
    using Y.condition4 X.condition4 by auto
next
  fix j q a b assume jq: "j ≤ q"  and "a ∈ Y q" and "b ∈ X q"
  thus "\<dd>y (Suc q) j (sy q j a) = a" and "\<dd>x (Suc q) j (sx q j b) = b"
    using Y.condition5 X.condition5 by auto
next
  fix j i q a b assume ji: "Suc j < i" and iq: "i ≤ q"  and "a ∈ Y q" and "b ∈ X q"
  thus "\<dd>y (Suc q) i (sy q j a) = sy (q - Suc 0) j (\<dd>y q (i - Suc 0) a)"
    and "\<dd>x (Suc q) i (sx q j b) = sx (q - Suc 0) j (\<dd>x q (i - Suc 0) b)"
    using Y.condition6 X.condition6
    by auto
qed

end

  (*TODO: Using the previous sublocale, prove the following lemma:*)

  (*
    instantiation prod :: (simplicial_set, simplicial_set) simplicial_set
    begin

    definition "X_prod = (λn. (X n::'a set) × (X n::'b set))"
    definition "\<dd>_prod = (λi n x. (\<dd> i n (fst x)::'a, \<dd> i n (snd x)::'b))"
    definition "s_prod = (λi n x. (s i n (fst x)::'a, s i n (snd x)::'b))"

    instance
    proof -
    interpret Y: simplicial_set "X::nat=>'a set" \<dd> s by unfold_locales
    interpret X: simplicial_set "X::nat=>'b set" \<dd> s by unfold_locales
    interpret Y_X: two_simplicial_sets "X::nat=>'a set" \<dd> s "X::nat=>'b set" \<dd> s by unfold_locales
    show "OFCLASS('a × 'b, simplicial_set_class)"
    unfolding class.simplicial_set_def X_prod_def \<dd>_prod_def s_prod_def
    apply intro_classes apply auto unfolding o_def apply auto
  *)

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

text{*The product $Y_{1} \times_{(t,f)} Y_{2}$ is a simplicial set*}

sublocale Y1_times_Y2_tf: simplicial_set 
  "(λn. {(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2})" 
  "(λi n x. (\<dd>y1 i n (fst x), \<dd>y2 i n (snd x)))" 
  "(λi n x. (sy1 i n (fst x), sy2 i n (snd x)))"
proof (unfold class.simplicial_set_def, auto)
  fix i q::nat and a b assume iq: "i ≤ Suc q" and a: "a ∈ Y1 (Suc q)"
  thus "\<dd>y1 (Suc q) i a ∈ Y1 q" using Y1.\<dd>_pi by auto
  assume b: "b ∈ Y2 (Suc q)"
  thus "\<dd>y2 (Suc q) i b ∈ Y2 q" using Y2.\<dd>_pi iq by auto
  assume ta_fb: "t (Suc q) a = f (Suc q) b"
  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)" .
next
  fix i q a b assume iq: "i ≤ q" and a: "a ∈ Y1 q" and b: "b ∈ Y2 q"
  thus "sy1 q i a ∈ Y1 (Suc q)" using Y1.s_pi by auto
  show "sy2 q i b ∈ Y2 (Suc q)" using iq b Y2.s_pi by auto
  assume ta_fb: "t q a = f q b" 
  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)" .
next
  fix q i j a b
  assume "0 < q " and "i < j" and "j ≤ Suc q" and "a ∈ Y1 (Suc q)" and "b ∈ Y2 (Suc q)"
  thus "\<dd>y1 q i (\<dd>y1 (Suc q) j a) = \<dd>y1 q (j - Suc 0) (\<dd>y1 (Suc q) i a)" 
    and  "\<dd>y2 q i (\<dd>y2 (Suc q) j b) = \<dd>y2 q (j - Suc 0) (\<dd>y2 (Suc q) i b)"
    using Y1.condition1 Y2.condition1 
    unfolding o_def fun_eq_iff by auto
next
  fix i j q a b
  assume "i ≤ j" and "j ≤ q" and "a ∈ Y1 q" and "b ∈ Y2 q"
  thus "sy1 (Suc q) i (sy1 q j a) = sy1 (Suc q) (Suc j) (sy1 q i a)"
    and "sy2 (Suc q) i (sy2 q j b) = sy2 (Suc q) (Suc j) (sy2 q i b)"
    using Y1.condition2 Y2.condition2 by auto
next
  fix i j q a b assume "i < j" and "j ≤ q" and "a ∈ Y1 q" and "b ∈ Y2 q"
  thus "\<dd>y1 (Suc q) i (sy1 q j a) = sy1 (q - Suc 0) (j - Suc 0) (\<dd>y1 q i a)"
    and "\<dd>y2 (Suc q) i (sy2 q j b) = sy2 (q - Suc 0) (j - Suc 0) (\<dd>y2 q i b)"
    using Y1.condition3 Y2.condition3 by auto
next
  fix j q a b assume jq: "j ≤ q" and "a ∈ Y1 q" and "b ∈ Y2 q"
  thus "\<dd>y1 (Suc q) (Suc j) (sy1 q j a) = a"
    and "\<dd>y2 (Suc q) (Suc j) (sy2 q j b) = b"
    and "\<dd>y1 (Suc q) j (sy1 q j a) = a"
    and "\<dd>y2 (Suc q) j (sy2 q j b) = b"
    using Y1.condition4 Y2.condition4
    using Y1.condition5 Y2.condition5
    by auto
next
  fix j i q a b assume "Suc j < i" and "i ≤ q" and "a ∈ Y1 q" and "b ∈ Y2 q"
  thus "\<dd>y1 (Suc q) i (sy1 q j a) = sy1 (q - Suc 0) j (\<dd>y1 q (i - Suc 0) a)"
    and "\<dd>y2 (Suc q) i (sy2 q j b) = sy2 (q - Suc 0) j (\<dd>y2 q (i - Suc 0) b)"
    using Y1.condition6 Y2.condition6
    by auto
qed


sublocale Y1_times_Y2_tf_Y1: two_simplicial_sets  
  "(λn. {(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2})" 
  "(λi n x. (\<dd>y1 i n (fst x), \<dd>y2 i n (snd x)))" 
  "(λi n x. (sy1 i n (fst x), sy2 i n (snd x)))" Y1 \<dd>y1 sy1 ..



(*I have had to include information about the domain.*)

(*
  lemma Y1_times_Y2_tf_Y1_morphism_fst: 
  shows "Y1_times_Y2_tf_Y1.morphism (λn x. fst x)"
  unfolding Y1_times_Y2_tf_Y1.morphism_def by auto
*)

lemma Y1_times_Y2_tf_Y1_morphism_fst: 
  shows "Y1_times_Y2_tf_Y1.morphism (λn. λx∈{(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2}. fst x)"
proof (auto simp add: Y1_times_Y2_tf_Y1.morphism_def Func_def)
  fix n i b a
  assume i: "i ≤ Suc n" and b: "b ∈ Y2 (Suc n)"
    and \<dd>y2_not_Y2: "\<dd>y2 (Suc n) i b ∉ Y2 n" 
  have "\<dd>y2 (Suc n) i b ∈ Y2 n" using b Y1_Y2_X.Y2.\<dd>_pi i by auto
  thus "undefined = \<dd>y1 (Suc n) i a" using \<dd>y2_not_Y2 by contradiction
next
  fix n i a b
  assume i: "i ≤ Suc n" and a: "a ∈ Y1 (Suc n)" and b: "b ∈ Y2 (Suc n)" and t_f: "t (Suc n) a = f (Suc n) b"
    and face: "\<dd>y1 (Suc n) i a ∉ Y1 n"
  have "\<dd>y1 (Suc n) i a ∈ Y1 n"  using a Y1_Y2_X.Y1.\<dd>_pi i by auto
  thus "undefined = \<dd>y1 (Suc n) i a" using face by contradiction
next
  fix n i a b assume i: "i ≤ Suc n" and a: "a ∈ Y1 (Suc n)" and b: "b ∈ Y2 (Suc n)"
    and tf: "t (Suc n) a = f (Suc n) b" and tf2: "t n (\<dd>y1 (Suc n) i a) ≠ f n (\<dd>y2 (Suc n) i b)"
  have "t n (\<dd>y1 (Suc n) i a) = f n (\<dd>y2 (Suc n) i b)"
    using Y1_times_Y2_tf.\<dd>_pi using a b tf i by (auto simp add: Pi_def)
  thus "undefined = \<dd>y1 (Suc n) i a" using tf2 by contradiction
next
  fix n i a b
  assume i: "i ≤ n" and b: "b ∈ Y2 n" and tf: "t n a = f n b" 
    and sy: "sy2 n i b ∉ Y2 (Suc n)"
  have "sy2 n i b ∈ Y2 (Suc n)" using b Y1_Y2_X.Y2.s_pi i by auto
  thus "undefined = sy1 n i a" using sy by contradiction
next
  fix n i a b
  assume i: "i ≤ n" and a: "a ∈ Y1 n" and b: "b ∈ Y2 n"
    and tf: "t n a = f n b" and sy: "sy1 n i a ∉ Y1 (Suc n)"
  have "sy1 n i a ∈ Y1 (Suc n)" using a Y1_Y2_X.Y1.s_pi i by auto
  thus "undefined = sy1 n i a" using sy by contradiction
next
  fix n i a b 
  assume i: "i ≤ n" and a: "a ∈ Y1 n" and b: "b ∈ Y2 n" and tf: "t n a = f n b"
    and tf2: "t (Suc n) (sy1 n i a) ≠ f (Suc n) (sy2 n i b)"
  have "t (Suc n) (sy1 n i a) = f (Suc n) (sy2 n i b)"
    using Y1_times_Y2_tf.s_pi using a b tf i by (auto simp add: Pi_def)
  thus "undefined = sy1 n i a" using tf2 by contradiction
qed

end

locale three_simplicial_sets_t_wo_f = Y1_Y2_X: three_simplicial_sets 
  + fixes t and f and ord
  assumes t: "Y1_X.morphism t"
  and f: "Y2_X.well_ordered_morphism (f,ord)"
begin

definition "X_Y1_Y2_tf_g 
  = (λn y1. {((a,b),(c,d)). a=y1 ∧ c=y1 ∧ y1 ∈ Y1 n ∧ b ∈ Y2 n ∧ d ∈ Y2 n ∧ t n y1 = f n b ∧ t n y1 = f n d ∧ (b,d) ∈ ord n (t n y1)})"

lemma refl_on_X_Y1_Y2_tf_g:
  shows "refl_on {y. (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) ∧ fst y = x} (X_Y1_Y2_tf_g n x)"
proof (unfold refl_on_def X_Y1_Y2_tf_g_def, auto)
  fix b assume x: "x ∈ Y1 n" and b: "b ∈ Y2 n" and tx_fb: "t n x = f n b"
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  thus "(b, b) ∈ ord n (f n b)" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def refl_on_def
    using b tx_fb by auto
qed

lemma trans_X_Y1_Y2_tf_g: "trans (X_Y1_Y2_tf_g n x)"
proof (unfold trans_def X_Y1_Y2_tf_g_def, auto)
  fix b ba bb assume x: "x ∈ Y1 n"  and tx_fba: "t n x = f n ba" and b_ba: "(b, ba) ∈ ord n (f n ba)"
    and fn_bb: "f n bb = f n ba" and fnb: "f n b = f n ba" and ba_bb: "(ba, bb) ∈ ord n (f n ba)"
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  hence trans_ord: "trans (ord n (t n x))" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by auto
  thus "(b, bb) ∈ ord n (f n ba)"  unfolding trans_def using b_ba ba_bb tx_fba by metis
qed


lemma antisym_X_Y1_Y2_tf_g: "antisym (X_Y1_Y2_tf_g n x)"
proof (unfold antisym_def X_Y1_Y2_tf_g_def, auto)
  fix b ba assume x: "x ∈ Y1 n" and tx_fba: "t n x = f n ba " and b_ba: " (b, ba) ∈ ord n (f n ba)"
    and fb_fba: " f n b = f n ba " and ba_b: " (ba, b) ∈ ord n (f n ba) " 
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  hence "antisym (ord n (t n x))" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by auto
  thus " b = ba" unfolding antisym_def
    by (metis b_ba ba_b tx_fba)
qed

lemma total_on_X_Y1_Y2_tf_g: "total_on {y. (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) ∧ fst y = x} 
  (X_Y1_Y2_tf_g n x)"
proof (unfold total_on_def X_Y1_Y2_tf_g_def, auto)
  fix b ba assume x: "x ∈ Y1 n" and b: "b ∈ Y2 n " and tx_fba: "t n x = f n ba " and ba: "ba ∈ Y2 n " 
    and fb_fba: "f n b = f n ba " and b_ba: "b ≠ ba " and ba_b: "(ba, b) ∉ ord n (f n ba) " 
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  hence "total_on  {y ∈ Y2 n. f n y = t n x} (ord n (t n x))" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by auto
  thus "(b, ba) ∈ ord n (f n ba)" unfolding total_on_def
    by (metis (mono_tags, lifting) b b_ba ba ba_b fb_fba mem_Collect_eq tx_fba)
qed

lemma Field_X_Y1_Y2_tf_g:
  "Field (X_Y1_Y2_tf_g n x)= {y. (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) ∧ fst y = x}"
  unfolding Field_def Domain_fst Range_snd image_def X_Y1_Y2_tf_g_def 
proof auto
  fix b assume x: "x ∈ Y1 n" and b: "b ∈ Y2 n"
    and tx_fb: "t n x = f n b" and "∀ba. f n b = f n ba --> ba ∈ Y2 n --> (ba, b) ∉ ord n (f n ba)"
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  hence "refl_on {y ∈ Y2 n. f n y = t n x} (ord n (t n x))" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by auto
  hence bb: "(b, b) ∈ ord n (f n b)" unfolding refl_on_def tx_fb using b by auto 
  show "∃ba. ba ∈ Y2 n ∧ f n b = f n ba ∧ (b, ba) ∈ ord n (f n b)"
    by (rule exI[of _ b], auto simp add: b bb)
qed


lemma Linear_order_X_Y1_Y2_tf_g: "Linear_order (X_Y1_Y2_tf_g n x)" 
  unfolding linear_order_on_def partial_order_on_def preorder_on_def
  using refl_on_X_Y1_Y2_tf_g trans_X_Y1_Y2_tf_g  refl_on_X_Y1_Y2_tf_g antisym_X_Y1_Y2_tf_g 
    total_on_X_Y1_Y2_tf_g Field_X_Y1_Y2_tf_g by auto

lemma wf_X_Y1_Y2_tf_g:
  assumes x: "x ∈ Y1 n"
  shows "wf (X_Y1_Y2_tf_g n x - Id)" 
proof -
  have t_Pi: "t n ∈ Y1 n -> X n" using t unfolding Y1_X.morphism_def Func_def by auto
  hence tnx: "t n x ∈ X n" using x by auto
  have ord_Pi: "(∀n. ord n ∈ Pi (X n) (%x. {r. well_order_on {y. y ∈ Y2 n ∧ f n y = x} r}))"
    using f unfolding Y2_X.well_ordered_morphism_def by auto
  hence wo: "well_order_on {y. y ∈ Y2 n ∧ f n y = t n x} (ord n (t n x))"
    using tnx by auto
  hence wf_ord: "wf (ord n (t n x) - Id)" 
    unfolding well_order_on_def linear_order_on_def partial_order_on_def preorder_on_def by auto
  have Field_ord: "Field (ord n (t n x)) = {y. y ∈ Y2 n ∧ f n y = t n x}"
    unfolding Field_def Domain_fst Range_snd image_def
  proof -
    have "fst ` ord n (t n x) ∪ snd ` ord n (t n x) = {R ∈ Y2 n. f n R = t n x}" 
      by (metis Domain_fst Field_def Range_snd well_order_on_Field wo)
    thus "{y. ∃x∈ord n (t n x). y = fst x} ∪ {y. ∃x∈ord n (t n x). y = snd x} 
      = {y ∈ Y2 n. f n y = t n x}" by (simp add: image_def)
  qed
  hence Wo: "Well_order (ord n (t n x))" using wo by auto
  hence Linear_order_ord: "Linear_order (ord n (t n x))" unfolding well_order_on_def by simp
  have exist_ord: "(∀A⊆Field (ord n (t n x)). A ≠ {} --> (∃a∈A. ∀a'∈A. (a, a') ∈ (ord n (t n x))))" 
    using wf_ord Linear_order_wf_diff_Id[OF Linear_order_ord] by simp  
  show ?thesis unfolding Linear_order_wf_diff_Id[OF Linear_order_X_Y1_Y2_tf_g]
  proof clarify
    fix A assume A_in_field: "A ⊆ Field (X_Y1_Y2_tf_g n x)" and A_not_empty: "A ≠ {}"
    have snd_A: "snd` A ⊆ Field (ord n (t n x))" 
      using A_in_field unfolding Field_ord Field_X_Y1_Y2_tf_g by auto
    have snd_A_not_empty: "snd` A ≠ {}" using A_not_empty by simp
    obtain a where a: "a ∈ snd` A" and a_min: "∀a'∈snd` A. (a, a') ∈ (ord n (t n x))"
      using exist_ord snd_A snd_A_not_empty by blast    
    show "∃a∈A. ∀a'∈A. (a, a') ∈ X_Y1_Y2_tf_g n x"
    proof (rule bexI[of _ "(x, a)"], auto)
      show "(x, a) ∈ A" using A_in_field a unfolding Field_X_Y1_Y2_tf_g by auto
      fix aa b assume aa_b_A: "(aa, b) ∈ A"
      show "((x, a), aa, b) ∈ X_Y1_Y2_tf_g n x" 
        using aa_b_A A_in_field a a_min unfolding Field_X_Y1_Y2_tf_g unfolding X_Y1_Y2_tf_g_def by auto
    qed
  qed
qed


lemma Well_order_X_Y1_Y2_tf_g:
  assumes x: "x ∈ Y1 n" 
  shows "Well_order (X_Y1_Y2_tf_g n x)" 
  by (metis Linear_order_X_Y1_Y2_tf_g well_order_on_def wf_X_Y1_Y2_tf_g x)

sublocale X_Y1_Y2_tf: three_simplicial_sets_tf X \<dd>x sx Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 t f
  using t f unfolding Y2_X.well_ordered_morphism_def by (unfold_locales, auto)

lemma Y1_times_Y2_tf_Y1_well_ordered_morphism_fst: 
(*  shows "X_Y1_Y2_tf.Y1_times_Y2_tf_Y1.well_ordered_morphism
  ((λn x. fst x), X_Y1_Y2_tf_g)"*)
  shows "X_Y1_Y2_tf.Y1_times_Y2_tf_Y1.well_ordered_morphism
  ((λn. λx∈{(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2}. fst x), X_Y1_Y2_tf_g)"
proof (unfold X_Y1_Y2_tf.Y1_times_Y2_tf_Y1.well_ordered_morphism_def, 
    auto simp add: Y1_times_Y2_tf_Y1_morphism_fst)
  fix n x assume x: "x ∈ Y1 n"
  have "well_order_on {y. (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) ∧ fst y = x} (X_Y1_Y2_tf_g n x)"
    unfolding well_order_on_def
    using Linear_order_X_Y1_Y2_tf_g wf_X_Y1_Y2_tf_g[OF x] 
    using Field_X_Y1_Y2_tf_g by auto
  moreover have "{y. ((case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) --> fst y = x) ∧
    (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2)} 
    = {y. (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) ∧ fst y = x}" 
    by auto
  ultimately show " well_order_on
    {y. ((case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2) --> fst y = x) ∧
    (case y of (y1, y2) => y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2)}
    (X_Y1_Y2_tf_g n x)" by simp
qed

definition "pullback_set = (λn. {(y1,y2). y1 ∈ Y1 n ∧ y2 ∈ Y2 n ∧ t n y1 = f n y2})"
definition "pullback_\<dd> = (λi n x. (\<dd>y1 i n (fst x), \<dd>y2 i n (snd x)))"
definition "pullback_s = (λi n x. (sy1 i n (fst x), sy2 i n (snd x)))"
definition "pullback = ((λn. λx ∈ pullback_set n. fst x)::(nat => 'b × 'c => 'b), X_Y1_Y2_tf_g)"

corollary well_ordered_morphism_pullback: 
  shows "X_Y1_Y2_tf.Y1_times_Y2_tf_Y1.well_ordered_morphism pullback" 
  using Y1_times_Y2_tf_Y1_well_ordered_morphism_fst 
  unfolding pullback_def pullback_set_def by simp

end

  (*
    Now we want to prove that the pullback respects the equivalence relation.
  *)

locale four_simplicial_sets_t = X: simplicial_set X \<dd>x sx 
  + X': simplicial_set X' \<dd>x' sx' + Y1: simplicial_set Y1 \<dd>y1 sy1 + Y2: simplicial_set Y2 \<dd>y2 sy2  
  for X::"nat => 'a set" 
  and \<dd>x :: "nat => nat => 'a => 'a"
  and sx :: "nat => nat => 'a => 'a"
  and X'::"nat => 'c set" 
  and \<dd>x' :: "nat => nat => 'c => 'c"
  and sx' :: "nat => nat => 'c => 'c"
  and Y1::"nat => 'b set" 
  and \<dd>y1 :: "nat => nat => 'b => 'b"
  and sy1 :: "nat => nat => 'b => 'b"
  and Y2::"nat => 'd set" 
  and \<dd>y2 :: "nat => nat => 'd => 'd"
  and sy2 :: "nat => nat => 'd => 'd" 
  + fixes t and f1 and ord1 and f2 and ord2 and f
  assumes t: "two_simplicial_sets.morphism X' \<dd>x' sx' X \<dd>x sx t"
  and iso_f: "three_simplicial_sets.iso_between_morphism X \<dd>x sx Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 (f1,ord1) (f2,ord2) f"
begin

sublocale X_Y1_Y2: three_simplicial_sets X \<dd>x sx Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 by unfold_locales
sublocale X_Y2_Y1: three_simplicial_sets X \<dd>x sx Y2 \<dd>y2 sy2 Y1 \<dd>y1 sy1 by unfold_locales
sublocale X_X'_Y1_t_f1: three_simplicial_sets_t_wo_f X \<dd>x sx X' \<dd>x' sx' Y1 \<dd>y1 sy1 t f1 ord1
  using t iso_f unfolding X_Y1_Y2.iso_between_morphism_def by (auto, unfold_locales)
sublocale X_X'_Y2_t_f2: three_simplicial_sets_t_wo_f X \<dd>x sx X' \<dd>x' sx' Y2 \<dd>y2 sy2 t f2 ord2
  using t iso_f unfolding X_Y1_Y2.iso_between_morphism_def by (unfold_locales, auto)
sublocale X_X'_Y1_t_f1: three_simplicial_sets_tf X \<dd>x sx X' \<dd>x' sx' Y1 \<dd>y1 sy1 t f1
  by unfold_locales

sublocale X'_X'Y1_X'Y2: three_simplicial_sets X' \<dd>x' sx' 
  X_X'_Y1_t_f1.pullback_set X_X'_Y1_t_f1.pullback_\<dd> X_X'_Y1_t_f1.pullback_s
  X_X'_Y2_t_f2.pullback_set X_X'_Y2_t_f2.pullback_\<dd> X_X'_Y2_t_f2.pullback_s
  unfolding X_X'_Y1_t_f1.pullback_set_def 
    X_X'_Y1_t_f1.pullback_\<dd>_def 
    X_X'_Y1_t_f1.pullback_s_def 
    X_X'_Y2_t_f2.pullback_set_def 
    X_X'_Y2_t_f2.pullback_\<dd>_def 
    X_X'_Y2_t_f2.pullback_s_def by unfold_locales

lemma f1_f2_in_rel2: 
  shows "(((f1,ord1),(Y1,\<dd>y1,sy1)), ((f2,ord2),(Y2,\<dd>y2,sy2))) ∈ X.rel2"
  unfolding X.rel2_def using iso_f by (auto, unfold_locales)

lemma morphism_pullback:
(*  "X'_X'Y1_X'Y2.Y1_Y2.morphism (λn x. (fst x, f n (snd x)))"*)
  "X'_X'Y1_X'Y2.Y1_Y2.morphism (λn. λx ∈ X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x)))"
proof (unfold X'_X'Y1_X'Y2.Y1_Y2.morphism_def, auto simp add: Func_def)
  fix n a b 
  assume "(a, b) ∈ X_X'_Y1_t_f1.pullback_set n" 
  thus "(a, f n b) ∈ X_X'_Y2_t_f2.pullback_set n"
    unfolding X_X'_Y1_t_f1.pullback_set_def X_X'_Y2_t_f2.pullback_set_def 
    using iso_f unfolding X_Y1_Y2.iso_between_morphism_def 
    unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def
    unfolding X_Y1_Y2.Y1_Y2.morphism_def Func_def by auto
next
  fix i n a b assume i_n: "i ≤ Suc n" and ab: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set (Suc n)"
  have b: "b ∈ Y1 (Suc n)" using ab unfolding X_X'_Y1_t_f1.pullback_set_def by auto
  show "(fst (X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, b)),
    f n (snd (X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, b)))) =
    X_X'_Y2_t_f2.pullback_\<dd> (Suc n) i (a, f (Suc n) b)"
    using iso_f i_n b
    unfolding X_X'_Y1_t_f1.pullback_\<dd>_def X_X'_Y2_t_f2.pullback_\<dd>_def b
    unfolding X_Y1_Y2.iso_between_morphism_def X_Y1_Y2.Y1_Y2.simplicial_set_iso_def
    unfolding X_Y1_Y2.Y1_Y2.morphism_def o_def by auto 
next
  fix i n a b assume i_n: "i ≤ n" and ab: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set n"
  have b: "b ∈ Y1 n" using ab unfolding X_X'_Y1_t_f1.pullback_set_def by auto
  show "(fst (X_X'_Y1_t_f1.pullback_s n i (a, b)),
    f (Suc n) (snd (X_X'_Y1_t_f1.pullback_s  n i (a, b)))) =
    X_X'_Y2_t_f2.pullback_s n i (a, f n b)"
    using b i_n iso_f
    unfolding X_X'_Y1_t_f1.pullback_s_def X_X'_Y2_t_f2.pullback_s_def
    unfolding  X_Y1_Y2.iso_between_morphism_def X_Y1_Y2.Y1_Y2.simplicial_set_iso_def
    unfolding X_Y1_Y2.Y1_Y2.morphism_def by auto
next
  fix n i a b
  assume ab_notin: "X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, b) ∉ X_X'_Y1_t_f1.pullback_set n"
    and i: "i ≤ Suc n" and ab_in: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set (Suc n)"
  have "X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, b) ∈ X_X'_Y1_t_f1.pullback_set n"
    using i ab_in X'_X'Y1_X'Y2.Y1.\<dd>_pi by auto
  thus "undefined = X_X'_Y2_t_f2.pullback_\<dd> (Suc n) i (a, f (Suc n) b)"
    using ab_notin by contradiction
next
  fix n i a b assume ab_notin: "X_X'_Y1_t_f1.pullback_s n i (a, b) ∉ X_X'_Y1_t_f1.pullback_set (Suc n)"
    and i: "i ≤ n" and ab_in: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set n"
  have "X_X'_Y1_t_f1.pullback_s n i (a, b) ∈ X_X'_Y1_t_f1.pullback_set (Suc n)" 
    using i ab_in X'_X'Y1_X'Y2.Y1.s_pi by auto
  thus "undefined = X_X'_Y2_t_f2.pullback_s n i (a, f n b)"
    using ab_notin by contradiction
qed

lemma inverse_pullback_morphism:
(*
  "∃g. X'_X'Y1_X'Y2.Y1_Y2.X_Y.morphism g 
  ∧ (∀n. (λx. (fst x, f n (snd x))) o g n = id ∧ g n o (λx. (fst x, f n (snd x))) = id)"
*)
  "∃g. X'_X'Y1_X'Y2.Y1_Y2.X_Y.morphism g ∧ (∀n. compose (X_X'_Y2_t_f2.pullback_set n) 
  (λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x))) (g n) = restrict id (X_X'_Y2_t_f2.pullback_set n) 
  ∧ compose (X_X'_Y1_t_f1.pullback_set n) (g n) 
  (λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x))) = restrict id (X_X'_Y1_t_f1.pullback_set n))"
proof - 
  obtain inv_f where inv_f: "X_Y2_Y1.iso_between_morphism (f2,ord2) (f1,ord1) inv_f" 
    and inv_f_id: "(∀n. compose (Y2 n) (f n) (inv_f n) = restrict id (Y2 n) 
    ∧ compose (Y1 n) (inv_f n) (f n) = restrict id (Y1 n))" 
    using X_Y1_Y2.sym_extended iso_f unfolding X.rel2_def by blast 
  let ?g="(λn. (λx∈X_X'_Y2_t_f2.pullback_set n. (fst x, inv_f n (snd x))))"
  let ?f="(λn. (λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x))))"
  have inverse_pullback_morphism: "X'_X'Y1_X'Y2.Y1_Y2.X_Y.morphism ?g"
    unfolding X'_X'Y1_X'Y2.Y1_Y2.X_Y.morphism_def Func_def
  proof auto
    fix n a b assume ab: "(a, b) ∈ X_X'_Y2_t_f2.pullback_set n" 
    thus "(a, inv_f n b) ∈ X_X'_Y1_t_f1.pullback_set n"      
    proof (unfold X_X'_Y1_t_f1.pullback_set_def X_X'_Y2_t_f2.pullback_set_def, auto)
      assume a: "a ∈ X' n" and b: "b ∈ Y2 n" and ta_f2b: "t n a = f2 n b" thus "inv_f n b ∈ Y1 n"
        using inv_f unfolding X_Y2_Y1.iso_between_morphism_def
        unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def
        unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def  Func_def
        by auto
      show "f2 n b = f1 n (inv_f n b)"
        using inv_f b unfolding X_Y2_Y1.iso_between_morphism_def
        unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def
        unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def fst_conv  
        by auto
    qed
  next
    fix n i a b assume i_n: "i ≤ Suc n" and ab: "(a, b) ∈ X_X'_Y2_t_f2.pullback_set (Suc n)"
    have b: "b ∈ Y2 (Suc n)" using ab unfolding X_X'_Y2_t_f2.pullback_set_def by simp
    show "(fst (X_X'_Y2_t_f2.pullback_\<dd>  (Suc n) i (a, b)),
      inv_f n (snd (X_X'_Y2_t_f2.pullback_\<dd>  (Suc n) i (a, b)))) =
      X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, inv_f (Suc n) b)"
      using b i_n inv_f
      unfolding X_X'_Y1_t_f1.pullback_\<dd>_def X_X'_Y2_t_f2.pullback_\<dd>_def
      unfolding X_Y2_Y1.iso_between_morphism_def 
      unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def
      unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def
      by auto
  next
    fix n i a b assume i_n: "i ≤ n" and ab: "(a, b) ∈ X_X'_Y2_t_f2.pullback_set n"
    have b: "b ∈ Y2 n" using ab unfolding X_X'_Y2_t_f2.pullback_set_def by simp
    show "(fst (X_X'_Y2_t_f2.pullback_s  n i (a, b)),
      inv_f (Suc n) (snd (X_X'_Y2_t_f2.pullback_s  n i (a, b)))) =
      X_X'_Y1_t_f1.pullback_s n i (a, inv_f n b)"
      using inv_f i_n b
      unfolding X_X'_Y1_t_f1.pullback_s_def X_X'_Y2_t_f2.pullback_s_def
      unfolding X_Y2_Y1.iso_between_morphism_def 
      unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def
      unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def
      by auto
  next
    fix n i a b
    assume ab_notin: "X_X'_Y2_t_f2.pullback_\<dd> (Suc n) i (a, b) ∉ X_X'_Y2_t_f2.pullback_set n"
      and i: "i ≤ Suc n" and ab_in: "(a, b) ∈ X_X'_Y2_t_f2.pullback_set (Suc n)"
    have "X_X'_Y2_t_f2.pullback_\<dd> (Suc n) i (a, b) ∈ X_X'_Y2_t_f2.pullback_set n"
      using i ab_in X'_X'Y1_X'Y2.Y2.\<dd>_pi by auto
    thus "undefined = X_X'_Y1_t_f1.pullback_\<dd> (Suc n) i (a, inv_f (Suc n) b)"
      using ab_notin by contradiction
  next
    fix n i a b
    assume ab_notin: "X_X'_Y2_t_f2.pullback_s n i (a, b) ∉ X_X'_Y2_t_f2.pullback_set (Suc n)"
      and i: "i ≤ n" and ab_in: "(a, b) ∈ X_X'_Y2_t_f2.pullback_set n"
    have "X_X'_Y2_t_f2.pullback_s n i (a, b) ∈ X_X'_Y2_t_f2.pullback_set  (Suc n)"
      using X'_X'Y1_X'Y2.Y2.s_pi i ab_in by auto
    thus "undefined = X_X'_Y1_t_f1.pullback_s n i (a, inv_f n b)"
      using ab_notin by contradiction
  qed
  moreover have "(∀n. compose (X_X'_Y2_t_f2.pullback_set n) (?f n) (?g n) = restrict id (X_X'_Y2_t_f2.pullback_set n) 
    ∧ compose (X_X'_Y1_t_f1.pullback_set n) (?g n) (?f n) = restrict id (X_X'_Y1_t_f1.pullback_set n))"
  proof (auto simp add: fun_eq_iff compose_def id_def)
    fix a b n assume ab_in: "(a, b) ∈ (X_X'_Y2_t_f2.pullback_set n)" 
    show "f n (inv_f n b) = b"
      using inv_f_id ab_in
      unfolding compose_def restrict_def 
      unfolding X_X'_Y2_t_f2.pullback_set_def
      by (auto, metis DEADID.map_id)
    assume notin: "(a, inv_f n b) ∉ X_X'_Y1_t_f1.pullback_set n"
    have "(a, inv_f n b) ∈ X_X'_Y1_t_f1.pullback_set n" 
      using ab_in inv_f 
      by  (simp add: X_X'_Y2_t_f2.pullback_set_def X_X'_Y1_t_f1.pullback_set_def 
        X_Y2_Y1.iso_between_morphism_def X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def 
        X_Y1_Y2.Y1_Y2.X_Y.morphism_def Func_def)
    thus "undefined = (a, b)" using notin by contradiction
  next
    fix n a b assume ab_in: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set n" 
    show "inv_f n (f n b) = b"
      using ab_in inv_f_id
      unfolding compose_def restrict_def
      unfolding X_X'_Y1_t_f1.pullback_set_def
      by (auto, metis DEADID.map_id)              
    assume notin: "(a, f n b) ∉ X_X'_Y2_t_f2.pullback_set n"
    have "(a, f n b) ∈ X_X'_Y2_t_f2.pullback_set n" 
      using iso_f ab_in
      unfolding X_X'_Y2_t_f2.pullback_set_def X_X'_Y1_t_f1.pullback_set_def
      unfolding X_Y1_Y2.iso_between_morphism_def
      unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def
      unfolding X_Y1_Y2.Y1_Y2.morphism_def
      unfolding Func_def by auto
    thus "undefined = (a, b)" using notin by contradiction      
  qed
  ultimately show ?thesis by auto
qed


lemma iso_between_morphism_pullback:
(*
  "X'_X'Y1_X'Y2.iso_between_morphism (X_X'_Y1_t_f1.pullback) (X_X'_Y2_t_f2.pullback) 
  (λn x. (fst x, f n (snd x)))"
*)
  "X'_X'Y1_X'Y2.iso_between_morphism (X_X'_Y1_t_f1.pullback) (X_X'_Y2_t_f2.pullback) 
  (λn. λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x)))"
proof (unfold X'_X'Y1_X'Y2.iso_between_morphism_def, auto)
  show "two_simplicial_sets.well_ordered_morphism (X_X'_Y1_t_f1.pullback_set) (X_X'_Y1_t_f1.pullback_\<dd>) 
    (X_X'_Y1_t_f1.pullback_s) X' \<dd>x' sx' (X_X'_Y1_t_f1.pullback)"
    unfolding X_X'_Y1_t_f1.pullback_set_def X_X'_Y1_t_f1.pullback_\<dd>_def 
      X_X'_Y1_t_f1.pullback_s_def
    by (metis X_X'_Y1_t_f1.well_ordered_morphism_pullback)
  show "two_simplicial_sets.well_ordered_morphism (X_X'_Y2_t_f2.pullback_set) (X_X'_Y2_t_f2.pullback_\<dd>) 
    (X_X'_Y2_t_f2.pullback_s) X' \<dd>x' sx' (X_X'_Y2_t_f2.pullback)"
    unfolding X_X'_Y2_t_f2.pullback_set_def X_X'_Y2_t_f2.pullback_\<dd>_def X_X'_Y2_t_f2.pullback_s_def
    by (metis X_X'_Y2_t_f2.well_ordered_morphism_pullback)
  show "X'_X'Y1_X'Y2.Y1_Y2.simplicial_set_iso (λn. λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x)))"
    using morphism_pullback
    unfolding X'_X'Y1_X'Y2.Y1_Y2.simplicial_set_iso_def 
    using inverse_pullback_morphism by auto
next
  fix n a b assume ab_in: "(a, b) ∈ X_X'_Y1_t_f1.pullback_set n"
  have "(a, f n b) ∈ X_X'_Y2_t_f2.pullback_set n"
    using ab_in iso_f 
    by (simp add: X_X'_Y2_t_f2.pullback_set_def X_X'_Y1_t_f1.pullback_set_def 
      X_Y1_Y2.iso_between_morphism_def X_Y1_Y2.Y1_Y2.simplicial_set_iso_def 
      X_Y1_Y2.Y1_Y2.morphism_def Func_def)
  thus "fst (X_X'_Y2_t_f2.pullback) n (a, f n b) = fst (X_X'_Y1_t_f1.pullback) n (a, b)"
    using ab_in
    unfolding X_X'_Y1_t_f1.pullback_def X_X'_Y2_t_f2.pullback_def by auto
next
  let ?g="(λn. λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x)))"
  obtain inv_f where inv_f: "X_Y2_Y1.iso_between_morphism (f2,ord2) (f1,ord1) inv_f"
    and inv_f_id: "∀n. compose (Y2 n) (f n) (inv_f n) = restrict id (Y2 n) 
    ∧ compose (Y1 n) (inv_f n) (f n) = restrict id (Y1 n)"
    by (metis X_Y1_Y2.sym_extended iso_f)
  fix x n assume x: "x ∈ X' n"
  have Wo1: "Well_order (X_X'_Y1_t_f1.X_Y1_Y2_tf_g n x)" 
    by (metis X_X'_Y1_t_f1.Linear_order_X_Y1_Y2_tf_g 
      X_X'_Y1_t_f1.wf_X_Y1_Y2_tf_g well_order_on_def x)
  have Wo2: "Well_order (X_X'_Y2_t_f2.X_Y1_Y2_tf_g n x)" 
    by (metis X_X'_Y2_t_f2.Well_order_X_Y1_Y2_tf_g x)
  have iso_ord1_ord2_f: "∀n. ∀x ∈ X n. iso (ord1 n x) (ord2 n x) (f n)" 
    using iso_f unfolding X_Y1_Y2.iso_between_morphism_def by simp
  show "iso (snd (X_X'_Y1_t_f1.pullback) n x) (snd (X_X'_Y2_t_f2.pullback) n x) (?g n)"
    unfolding X_X'_Y1_t_f1.pullback_def X_X'_Y2_t_f2.pullback_def
    unfolding snd_conv
  proof -    
    show "iso (X_X'_Y1_t_f1.X_Y1_Y2_tf_g n x) (X_X'_Y2_t_f2.X_Y1_Y2_tf_g n x) (?g n)"
      unfolding iso_iff3[OF Wo1 Wo2] 
    proof auto
      show "bij_betw (?g n) (Field (X_X'_Y1_t_f1.X_Y1_Y2_tf_g n x))
        (Field (X_X'_Y2_t_f2.X_Y1_Y2_tf_g n x))" unfolding bij_betw_def 
        unfolding X_X'_Y2_t_f2.Field_X_Y1_Y2_tf_g
        unfolding X_X'_Y1_t_f1.Field_X_Y1_Y2_tf_g
        unfolding inj_on_def image_def 
        unfolding X_X'_Y1_t_f1.pullback_set_def
      proof auto
        fix b ba assume "b ∈ Y1 n"
          and "t n x = f1 n ba" and ba: "ba ∈ Y1 n" and f1: "f1 n b = f1 n ba" and "f n b = f n ba"
        show "b = ba" using iso_ord1_ord2_f unfolding iso_def bij_betw_def 
          by (metis (erased, lifting) X_Y1_Y2.Y1_Y2.simplicial_set_iso_bij 
            X_Y1_Y2.iso_between_morphism_def `b ∈ Y1 n` `f n b = f n ba` 
            ba bij_betw_def inj_on_contraD iso_f)
      next
        fix ba assume ba: "ba ∈ Y1 n" and tx_f1ba: "t n x = f1 n ba" 
        thus "f n ba ∈ Y2 n" 
          using iso_f unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def 
          unfolding X_Y1_Y2.Y1_Y2.morphism_def Func_def by auto
        show "f1 n ba = f2 n (f n ba)" using ba tx_f1ba
          using iso_f unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def X_Y1_Y2.Y1_Y2.morphism_def by auto
      next
        fix b
        assume b: "b ∈ Y2 n" and tx_f2b: "t n x = f2 n b"
        show "∃a. a ∈ X' n ∧ (∃ba. ba ∈ Y1 n ∧ t n a = f1 n ba ∧ a = x ∧ b = f n ba)"
        proof (rule exI[of _ x], auto simp add: x, rule exI[of _ "inv_f n b"], auto)
          show "inv_f n b ∈ Y1 n"
            using inv_f b unfolding X_Y2_Y1.iso_between_morphism_def
            unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def 
            unfolding X_Y1_Y2.Y1_Y2.X_Y.morphism_def Func_def by auto
          show "t n x = f1 n (inv_f n b)" 
            using inv_f b unfolding X_Y2_Y1.iso_between_morphism_def
            unfolding X_Y1_Y2.Y1_Y2.X_Y.simplicial_set_iso_def 
            unfolding fst_conv tx_f2b by auto
          show "b = f n (inv_f n b)" 
            using inv_f_id b unfolding compose_def restrict_def id_def by metis
        qed
      qed
      show "compat (X_X'_Y1_t_f1.X_Y1_Y2_tf_g n x) (X_X'_Y2_t_f2.X_Y1_Y2_tf_g n x) (?g n)"
        unfolding compat_def X_X'_Y1_t_f1.X_Y1_Y2_tf_g_def X_X'_Y2_t_f2.X_Y1_Y2_tf_g_def
        unfolding X_X'_Y1_t_f1.pullback_set_def
      proof auto
        fix b assume b: "b ∈ Y1 n"
        thus "f n b ∈ Y2 n"
          using iso_f unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def X_Y1_Y2.Y1_Y2.morphism_def Func_def
          by auto
        fix ba 
        assume ba: "ba ∈ Y1 n"
        thus "f n ba ∈ Y2 n"
          using iso_f unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def X_Y1_Y2.Y1_Y2.morphism_def Func_def 
          by auto       
        show "f1 n b = f2 n (f n b)" using iso_f b unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def X_Y1_Y2.Y1_Y2.morphism_def by auto
        assume f1ba_f1b: "f1 n ba = f1 n b"
        thus "f1 n b = f2 n (f n ba)" using ba using iso_f  unfolding X_Y1_Y2.iso_between_morphism_def 
          unfolding X_Y1_Y2.Y1_Y2.simplicial_set_iso_def X_Y1_Y2.Y1_Y2.morphism_def by auto
      next
        fix b ba
        assume f1_eq: "f1 n b = f1 n ba" and b: "b ∈ Y1 n"
          and b_ba: "(b, ba) ∈ ord1 n (f1 n ba)"
        have f1b_in_X: "f1 n b ∈ X n" 
          using iso_f b unfolding X_Y1_Y2.iso_between_morphism_def
          unfolding X_Y1_Y2.Y1_X.well_ordered_morphism_def X_Y1_Y2.Y1_X.morphism_def Func_def 
          by auto
        hence compat_f: "compat (ord1 n (f1 n b)) (ord2 n (f1 n b)) (f n)" 
          using iso_ord1_ord2_f 
          using iso_iff3[OF X_Y1_Y2.Well_order_ord1[OF f1b_in_X iso_f] 
            X_Y1_Y2.Well_order_ord2[OF f1b_in_X iso_f]] by auto
        show "(f n b, f n ba) ∈ ord2 n (f1 n ba)"
          using compat_f b_ba unfolding compat_def f1_eq by auto
      qed
    qed
  qed
qed


lemma pullback_preserves_rel:
  "((X_X'_Y1_t_f1.pullback,(X_X'_Y1_t_f1.pullback_set,X_X'_Y1_t_f1.pullback_\<dd>,X_X'_Y1_t_f1.pullback_s)),
  (X_X'_Y2_t_f2.pullback, (X_X'_Y2_t_f2.pullback_set, X_X'_Y2_t_f2.pullback_\<dd>,X_X'_Y2_t_f2.pullback_s))) ∈ X'.rel2" 
proof (unfold X'.rel2_def, auto)
  let ?g="(λn. λx∈X_X'_Y1_t_f1.pullback_set n. (fst x, f n (snd x)))"
  show "class.simplicial_set X_X'_Y1_t_f1.pullback_set X_X'_Y1_t_f1.pullback_\<dd> X_X'_Y1_t_f1.pullback_s" 
    unfolding X_X'_Y1_t_f1.pullback_set_def X_X'_Y1_t_f1.pullback_\<dd>_def X_X'_Y1_t_f1.pullback_s_def
    by unfold_locales
  show "class.simplicial_set X_X'_Y2_t_f2.pullback_set X_X'_Y2_t_f2.pullback_\<dd> X_X'_Y2_t_f2.pullback_s" 
    unfolding X_X'_Y2_t_f2.pullback_set_def X_X'_Y2_t_f2.pullback_\<dd>_def X_X'_Y2_t_f2.pullback_s_def
    by unfold_locales
  have "X'_X'Y1_X'Y2.iso_between_morphism (X_X'_Y1_t_f1.pullback) (X_X'_Y2_t_f2.pullback) ?g"
    using iso_between_morphism_pullback .
  thus "Ex (X'_X'Y1_X'Y2.iso_between_morphism (X_X'_Y1_t_f1.pullback) (X_X'_Y2_t_f2.pullback))"
    by auto
qed
end

locale X'_X_t = X'_X: two_simplicial_sets X' \<dd>x' sx' X \<dd>x sx
  for X'::"nat => 'b set" 
  and \<dd>x' :: "nat => nat => 'b => 'b"
  and sx' :: "nat => nat => 'b => 'b"
  and X::"nat => 'a set" 
  and \<dd>x :: "nat => nat => 'a => 'a"
  and sx :: "nat => nat => 'a => 'a"
  + fixes t assumes t: "morphism t"
begin

(* 
  I try to define t*. I call it t' because it is not allowed to write t* in a function name.
*)

definition "t_aux A = 
  (let f=fst (fst A); ord = snd (fst A); Y=fst (snd A); \<dd>y = fst (snd (snd A)); sy = snd (snd (snd A))
  in (three_simplicial_sets_t_wo_f.pullback X' Y t f ord,
  (three_simplicial_sets_t_wo_f.pullback_set X' Y t f,
  three_simplicial_sets_t_wo_f.pullback_\<dd> \<dd>x' \<dd>y,
  three_simplicial_sets_t_wo_f.pullback_s sx' sy
  ))
  )"


definition t'::"(((nat => 'c => 'a) × (nat => 'a => ('c × 'c) set)) × (nat => 'c set) × (nat => nat => 'c => 'c) × (nat => nat => 'c => 'c)) set
  => (((nat => ('b × 'c) => 'b) × (nat => 'b => (('b × 'c) × ('b × 'c)) set)) × (nat => ('b × 'c) set) × (nat => nat => ('b × 'c) => ('b × 'c)) × (nat => nat => ('b × 'c) => ('b × 'c))) set"
  where "t' S = {b. ∃a∈S. (b, t_aux a) ∈ simplicial_set.rel2 X' \<dd>x' sx'}"



(*
  Y.W is simplicial_set.W X' \<dd>x' sx', maybe I should change the names of the sublocale to first, second...
  in order no to be named Y when really in this case is X'.
  The following lemma claims that t' goes from W(X) to W(X')
*)

lemma t'_Pi_quotients: "t' ∈ X.W -> Y.W" (*Types of X.W and Y.W are different, if not we cannot prove it since pullback is used.*)
proof (unfold X.W_def Y.W_def Pi_def quotient_def, auto)
  fix f1 ord1 \<dd>y1 sy1 and Y1 :: "nat => 'c set"
  assume in_X_W1: "((f1, ord1), Y1, \<dd>y1, sy1) ∈ X.W1'"
  interpret Y1_X: two_simplicial_sets Y1 \<dd>y1 sy1 X \<dd>x sx
    using in_X_W1 unfolding X.W1'_def two_simplicial_sets_def by (auto, unfold_locales) 
  interpret X'_Y_t_f1: three_simplicial_sets_t_wo_f X \<dd>x sx X' \<dd>x' sx' Y1 \<dd>y1 sy1 t f1 ord1 
    using in_X_W1 t unfolding X.W1'_def  unfolding three_simplicial_sets_t_wo_f_def
      three_simplicial_sets_def three_simplicial_sets_t_wo_f_axioms_def by (auto, intro_locales)
  def p ≡ "(three_simplicial_sets_t_wo_f.pullback X' Y1 t f1 ord1, 
    (three_simplicial_sets_t_wo_f.pullback_set X' Y1 t f1, 
    three_simplicial_sets_t_wo_f.pullback_\<dd> \<dd>x' \<dd>y1, 
    three_simplicial_sets_t_wo_f.pullback_s sx' sy1
    ))"
  show "∃x::((nat => 'b × 'c => 'b) × (nat => 'b => (('b × 'c) × 'b × 'c) set)) ×
    (nat => ('b × 'c) set) × (nat => nat => 'b × 'c => 'b × 'c) × (nat => nat => 'b × 'c => 'b × 'c) 
    ∈ simplicial_set.W1' X' \<dd>x' sx'. t' (simplicial_set.rel2 X \<dd>x sx `` {((f1, ord1), Y1, \<dd>y1, sy1)}) 
    = (simplicial_set.rel2 X' \<dd>x' sx' `` {x}::(((nat => ('b × 'c) => 'b) 
    × (nat => 'b => (('b × 'c) × ('b × 'c)) set)) × (nat => ('b × 'c) set) 
    × (nat => nat => ('b × 'c) => ('b × 'c)) × (nat => nat => ('b × 'c) => ('b × 'c))) set)"
  proof (rule bexI[of _ p])
    show "p ∈ simplicial_set.W1' X' \<dd>x' sx'"
      unfolding p_def Y.W1'_def
    proof auto
      show "class.simplicial_set (X'_Y_t_f1.pullback_set) (X'_Y_t_f1.pullback_\<dd>) (X'_Y_t_f1.pullback_s)" 
        unfolding X'_Y_t_f1.pullback_set_def X'_Y_t_f1.pullback_\<dd>_def X'_Y_t_f1.pullback_s_def
        by unfold_locales
      show "two_simplicial_sets.well_ordered_morphism 
        (X'_Y_t_f1.pullback_set) (X'_Y_t_f1.pullback_\<dd>) (X'_Y_t_f1.pullback_s) 
        X' \<dd>x' sx' (X'_Y_t_f1.pullback)" using X'_Y_t_f1.Y1_times_Y2_tf_Y1_well_ordered_morphism_fst
        unfolding X'_Y_t_f1.pullback_set_def X'_Y_t_f1.pullback_\<dd>_def 
        unfolding X'_Y_t_f1.pullback_s_def X'_Y_t_f1.pullback_def X'_Y_t_f1.pullback_set_def .
    qed
      (*
        This show works, but the elements of simplicial_set.rel2 can be of different types. Two properties appear,
        I can demonstrate the first one (transitivity), but the second one do not (because I need to relate f with itself, hence 
        the relation must be of the same types). This las property is indeed stating that the function goes to the quotient set (hence, the 
        related elements must be of the same type).

        show "t' (simplicial_set.rel2 X \<dd>x sx `` {((f1, ord1), Y1, \<dd>y1, sy1)}) 
        = simplicial_set.rel2 X' \<dd>x' sx' `` {p}"
      *)

      (* 
        So we have to explicitly fix the types again.
      *)
    show "t' (simplicial_set.rel2 X \<dd>x sx `` {((f1, ord1), Y1, \<dd>y1, sy1)}) = (simplicial_set.rel2 X' \<dd>x' sx' `` {p}
      ::(((nat => ('b × 'c) => 'b) × (nat => 'b => (('b × 'c) × ('b × 'c)) set)) × (nat => ('b × 'c) set) 
      × (nat => nat => ('b × 'c) => ('b × 'c)) × (nat => nat => ('b × 'c) => ('b × 'c))) set)"
      unfolding t'_def unfolding Image_def image_def 
    proof (auto)
      fix f2 ord2 \<dd>y2 sy2 and Y2 and a b aa ab ba
      assume f1_f2_in_rel2: "(((f1, ord1), Y1, \<dd>y1, sy1), (f2, ord2), Y2, \<dd>y2, sy2) ∈ X.rel2"
        and a_f2_X'_rel2: "(((a, b), aa, ab, ba), t_aux ((f2, ord2), Y2, \<dd>y2, sy2)) ∈ simplicial_set.rel2 X' \<dd>x' sx'"
      interpret aa: simplicial_set aa ab ba using a_f2_X'_rel2 unfolding Y.rel2_def by auto
      interpret X_Y1_Y2: three_simplicial_sets X \<dd>x sx Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 
        using f1_f2_in_rel2 unfolding X.rel2_def
        unfolding  three_simplicial_sets_def by (auto, unfold_locales)
      interpret Y2_X: two_simplicial_sets Y2 \<dd>y2 sy2 X \<dd>x sx
        using f1_f2_in_rel2 unfolding X.rel2_def two_simplicial_sets_def by (auto, intro_locales)
      obtain f where iso_f: "X_Y1_Y2.iso_between_morphism (f1,ord1) (f2, ord2) f"
        using f1_f2_in_rel2 unfolding X.rel2_def by auto
      interpret X'_Y_t_f2: three_simplicial_sets_t_wo_f X \<dd>x sx X' \<dd>x' sx' Y2 \<dd>y2 sy2 t f2 ord2 
        unfolding three_simplicial_sets_t_wo_f_def three_simplicial_sets_t_wo_f_axioms_def
        using t f1_f2_in_rel2 iso_f unfolding X.rel2_def X_Y1_Y2.iso_between_morphism_def
        by (auto, unfold_locales)
      interpret X_X'_Y1_Y2_t_f: four_simplicial_sets_t X \<dd>x sx X' \<dd>x' sx' Y1 \<dd>y1 sy1 Y2 \<dd>y2 sy2 t f1 ord1 f2 ord2 f 
        using iso_f f1_f2_in_rel2 t unfolding X.rel2_def
        unfolding four_simplicial_sets_t_def four_simplicial_sets_t_axioms_def 
        by (auto, intro_locales)
      interpret X'_aa_X'Y2: three_simplicial_sets X' \<dd>x' sx' aa ab ba X'_Y_t_f2.pullback_set X'_Y_t_f2.pullback_\<dd> X'_Y_t_f2.pullback_s
        using a_f2_X'_rel2 unfolding Y.rel2_def
        unfolding X'_Y_t_f2.pullback_set_def X'_Y_t_f2.pullback_\<dd>_def X'_Y_t_f2.pullback_s_def
        by unfold_locales
      interpret X'_X'Y2_aa: three_simplicial_sets X' \<dd>x' sx' X'_Y_t_f2.pullback_set X'_Y_t_f2.pullback_\<dd> X'_Y_t_f2.pullback_s aa ab ba
        using a_f2_X'_rel2 unfolding Y.rel2_def
        unfolding X'_Y_t_f2.pullback_set_def X'_Y_t_f2.pullback_\<dd>_def X'_Y_t_f2.pullback_s_def
        by unfold_locales
      interpret X'_X'Y1_aa: three_simplicial_sets X' \<dd>x' sx' X'_Y_t_f1.pullback_set X'_Y_t_f1.pullback_\<dd> X'_Y_t_f1.pullback_s aa ab ba
        using a_f2_X'_rel2 unfolding Y.rel2_def
        unfolding X'_Y_t_f2.pullback_set_def X'_Y_t_f2.pullback_\<dd>_def X'_Y_t_f2.pullback_s_def
        by unfold_locales
      interpret X'_X'Y1_X'Y2_aa: four_simplicial_sets X' \<dd>x' sx' X'_Y_t_f1.pullback_set X'_Y_t_f1.pullback_\<dd> X'_Y_t_f1.pullback_s 
        X'_Y_t_f2.pullback_set X'_Y_t_f2.pullback_\<dd> X'_Y_t_f2.pullback_s aa ab ba
        unfolding X'_Y_t_f1.pullback_set_def X'_Y_t_f1.pullback_\<dd>_def X'_Y_t_f1.pullback_s_def
        unfolding X'_Y_t_f2.pullback_set_def X'_Y_t_f2.pullback_\<dd>_def X'_Y_t_f2.pullback_s_def
        by intro_locales
      def p2≡"(X'_Y_t_f2.pullback, (X'_Y_t_f2.pullback_set, X'_Y_t_f2.pullback_\<dd>, X'_Y_t_f2.pullback_s))" 
      obtain F where iso_F: "X'_aa_X'Y2.iso_between_morphism (a,b) X'_Y_t_f2.pullback F" 
        using a_f2_X'_rel2 unfolding Y.rel2_def t_aux_def by auto
      obtain G where G: "X'_X'Y2_aa.iso_between_morphism X'_Y_t_f2.pullback (a,b) G" 
        using X'_aa_X'Y2.sym_extended[of a b "fst X'_Y_t_f2.pullback" "snd X'_Y_t_f2.pullback" F] using iso_F
        by auto
      have p_p2: "(p, p2) ∈ simplicial_set.rel2 X' \<dd>x' sx'" 
        using X_X'_Y1_Y2_t_f.pullback_preserves_rel unfolding p_def p2_def by auto
      from this obtain H 
        where H: "X_X'_Y1_Y2_t_f.X'_X'Y1_X'Y2.iso_between_morphism X'_Y_t_f1.pullback X'_Y_t_f2.pullback H"
        unfolding p_def p2_def Y.rel2_def by force
      obtain J where J: "X'_X'Y1_aa.iso_between_morphism X'_Y_t_f1.pullback (a,b) J"
        using X'_X'Y1_X'Y2_aa.trans_extended H G using surjective_pairing by metis
      show "(p, (a, b), aa, ab, ba) ∈ simplicial_set.rel2 X' \<dd>x' sx'" term p term aa
      proof (unfold Y.rel2_def p_def, auto)
        show "class.simplicial_set (X'_Y_t_f1.pullback_set) (X'_Y_t_f1.pullback_\<dd>) (X'_Y_t_f1.pullback_s)"
          unfolding X'_Y_t_f1.pullback_set_def X'_Y_t_f1.pullback_\<dd>_def X'_Y_t_f1.pullback_s_def 
          by unfold_locales
        show "class.simplicial_set aa ab ba" using a_f2_X'_rel2 unfolding Y.rel2_def by auto          
        show "Ex (three_simplicial_sets.iso_between_morphism X' \<dd>x' sx' (X'_Y_t_f1.pullback_set)
          (X'_Y_t_f1.pullback_\<dd>) (X'_Y_t_f1.pullback_s) aa ab ba (X'_Y_t_f1.pullback) (a, b))"
          using J by auto
      qed
    next
      fix a::"nat => 'b × 'c => 'b" and b aa ab ba
      assume pa: "(p, (a, b), aa, ab, ba) ∈ simplicial_set.rel2 X' \<dd>x' sx'"
      show "∃(ac::nat=>'c=>'a) bb ad ae bc.
        (((f1, ord1), Y1, \<dd>y1, sy1), (ac, bb), ad, ae, bc) ∈ simplicial_set.rel2 X \<dd>x sx ∧
        (((a, b), aa, ab, ba), t_aux ((ac, bb), ad, ae, bc)) ∈ simplicial_set.rel2 X' \<dd>x' sx'"
      proof (rule exI[of _ f1],rule exI[of _ ord1],rule exI[of _ Y1],rule exI[of _ \<dd>y1],rule exI[of _ sy1], auto)
        show "(((f1, ord1), Y1, \<dd>y1, sy1), (f1, ord1), Y1, \<dd>y1, sy1) ∈ simplicial_set.rel2 X \<dd>x sx"
          by (metis X.refl_on_W1'_rel2 in_X_W1 refl_onD)
        show "(((a, b), aa, ab, ba), t_aux ((f1, ord1), Y1, \<dd>y1, sy1)) ∈ simplicial_set.rel2 X' \<dd>x' sx'"
          unfolding t_aux_def using pa by (auto, metis Y.sym_rel2 p_def symD)
      qed
    qed
  qed
qed

end

end