---

Step * 2 of Lemma glue-morph-comp


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. ¬(phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K)))
13. u : glue-cube(Gamma;A;phi;T;w;I;rho)
⊢ glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
= glue-morph(Gamma;A;phi;T;w;I;rho;K;f ⋅ g;u)
∈ (J1:fset(ℕ) ⟶ f1:{f1:J1 ⟶ K| phi(f1(f ⋅ g(rho))) = 1 ∈ Point(face_lattice(J1))}  ⟶ T(f1(f ⋅ g(rho)))
  × A(f ⋅ g(rho)))
BY
{ ((Unfold `glue-cube` -1 THEN Unfold `glue-morph` 0) THEN (Assert ⌜(phi(f(rho))==1) ~ ff⌝⋅ THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. ¬(phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K)))
13. u : if (phi(rho)==1)
then T(rho)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
      let t,a = ta 
      in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
fi 
⊢ (phi(f(rho))==1) = ff

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. I : fset(ℕ)
7. rho : Gamma(I)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. ¬(phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K)))
13. u : if (phi(rho)==1)
then T(rho)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
      let t,a = ta 
      in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
fi 
14. (phi(f(rho))==1) ~ ff
⊢ if (phi(f(rho))==1)
then (if (phi(rho)==1)
     then (u rho f)
     else let t,a = u 
          in if (phi(f(rho))==1) then t J f else <λK,g. (t K f ⋅ g), (a rho f)> fi 
     fi  f(rho) g)
else let t,a = if (phi(rho)==1)
     then (u rho f)
     else let t,a = u 
          in if (phi(f(rho))==1) then t J f else <λK,g. (t K f ⋅ g), (a rho f)> fi 
     fi  
     in if (phi(g(f(rho)))==1) then t K g else <λK@0,g@0. (t K@0 g ⋅ g@0), (a f(rho) g)> fi 
fi 
= if (phi(rho)==1)
  then (u rho f ⋅ g)
  else let t,a = u 
       in if (phi(f ⋅ g(rho))==1) then t K f ⋅ g else <λK@0,g@0. (t K@0 f ⋅ g ⋅ g@0), (a rho f ⋅ g)> fi 
  fi 
∈ (J1:fset(ℕ) ⟶ f1:{f1:J1 ⟶ K| phi(f1(f ⋅ g(rho))) = 1 ∈ Point(face_lattice(J1))}  ⟶ T(f1(f ⋅ g(rho)))
  × A(f ⋅ g(rho)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  T  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  w  :  \{Gamma,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
6.  I  :  fset(\mBbbN{})
7.  rho  :  Gamma(I)
8.  J  :  fset(\mBbbN{})
9.  K  :  fset(\mBbbN{})
10.  f  :  J  {}\mrightarrow{}  I
11.  g  :  K  {}\mrightarrow{}  J
12.  \mneg{}(phi(f  \mcdot{}  g(rho))  =  1)
13.  u  :  glue-cube(Gamma;A;phi;T;w;I;rho)
\mvdash{}  glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
=  glue-morph(Gamma;A;phi;T;w;I;rho;K;f  \mcdot{}  g;u)


By

---

Latex:
((Unfold  `glue-cube`  -1  THEN  Unfold  `glue-morph`  0)
  THEN  (Assert  \mkleeneopen{}(phi(f(rho))==1)  \msim{}  ff\mkleeneclose{}\mcdot{}  THENA  Auto)
  )

---

Home Index