---

Step * 1 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. u : glue-cube(Gamma;A;phi;T;w;I;rho)
13. phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K))
⊢ 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)
∈ T(f ⋅ g(rho))
BY
{ (Unfold `glue-cube` -2 THEN Unfold `glue-morph` 0 THEN (BoolCase ⌜(phi(rho)==1)⌝⋅ 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. 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 
13. phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K))
14. phi(rho) = 1 ∈ Point(face_lattice(I))
⊢ if (phi(f(rho))==1)
then ((u rho f) f(rho) g)
else let t,a = (u rho f) 
     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 
= (u rho f ⋅ g)
∈ T(f ⋅ g(rho))

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. ¬(phi(rho) = 1 ∈ Point(face_lattice(I)))
9. J : fset(ℕ)
10. K : fset(ℕ)
11. f : J ⟶ I
12. g : K ⟶ J
13. u : {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)} 
14. phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K))
⊢ if (phi(f(rho))==1)
then (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  f(rho) g)
else let t,a = 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  
     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 
= 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 
∈ T(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.  u  :  glue-cube(Gamma;A;phi;T;w;I;rho)
13.  phi(f  \mcdot{}  g(rho))  =  1
\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`  -2  THEN  Unfold  `glue-morph`  0  THEN  (BoolCase  \mkleeneopen{}(phi(rho)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index