---

Step * 2 of Lemma glue-term_wf


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A}
8. app(w; t) = a ∈ {Gamma, phi ⊢ _:A}
9. glue [phi ⊢→ t] a ∈ I:fset(ℕ) ⟶ a:Gamma(I) ⟶ Glue [phi ⊢→ (T;w)] A(a)
⊢ glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
BY
{ (MemTypeCD
   THEN Auto
   THEN RepUR ``glue-type`` (-5)
   THEN RenameVar `rho' (-1)
   THEN RepUR ``glue-type`` 0
   THEN BLemma `equal-glue-cube`
   THEN Auto
   THEN RepUR ``glue-term 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. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A}
8. app(w; t) = a ∈ {Gamma, phi ⊢ _:A}
9. glue [phi ⊢→ t] a ∈ I:fset(ℕ) ⟶ a:Gamma(I) ⟶ glue-cube(Gamma;A;phi;T;w;I;a)
10. I : fset(ℕ)
11. J : fset(ℕ)
12. f : J ⟶ I
13. rho : Gamma(I)
14. phi(rho) = 1 ∈ Point(face_lattice(I))
⊢ if (phi(f(rho))==1)
then (t(rho) rho f) = if (phi(f(rho))==1) then t(f(rho)) else <λJ@0,f@0. t(f@0(f(rho))), a(f(rho))> fi  ∈ T(f(rho))
else (t(rho) rho f)
     = if (phi(f(rho))==1) then t(f(rho)) else <λJ@0,f@0. t(f@0(f(rho))), a(f(rho))> fi 
     ∈ (J1:fset(ℕ) ⟶ f1:{f1:J1 ⟶ J| phi(f1(f(rho))) = 1 ∈ Point(face_lattice(J1))}  ⟶ T(f1(f(rho))) × A(f(rho)))
fi 

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

---

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.  t  :  \{Gamma,  phi  \mvdash{}  \_:T\}
7.  a  :  \{Gamma  \mvdash{}  \_:A\}
8.  app(w;  t)  =  a
9.  glue  [phi  \mvdash{}\mrightarrow{}  t]  a  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:Gamma(I)  {}\mrightarrow{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A(a)
\mvdash{}  glue  [phi  \mvdash{}\mrightarrow{}  t]  a  \mmember{}  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}


By

---

Latex:
(MemTypeCD
  THEN  Auto
  THEN  RepUR  ``glue-type``  (-5)
  THEN  RenameVar  `rho'  (-1)
  THEN  RepUR  ``glue-type``  0
  THEN  BLemma  `equal-glue-cube`
  THEN  Auto
  THEN  RepUR  ``glue-term  glue-morph``  0
  THEN  (BoolCase  \mkleeneopen{}(phi(rho)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index