---

Step * 2 of Lemma glue-equations_wf

.....subterm..... T:t
2:n
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(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) ∈ Type
9. t : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho))
10. a : A(rho)
⊢ ∀J:fset(ℕ). ∀f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} .
    ((w(f(rho)) J 1 (t J f)) = (a rho f) ∈ A(f(rho))) ∈ ℙ
BY
{ RepeatFor 2 (((MemCD THENW Auto) THENL [Auto;  Id])) }

1
.....subterm..... T:t
2:n
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(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) ∈ Type
9. t : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho))
10. a : A(rho)
11. J : fset(ℕ)
12. f : {f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} 
⊢ (w(f(rho)) J 1 (t J f)) = (a rho f) ∈ A(f(rho)) ∈ ℙ

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}    {}\mrightarrow{}  T(f(rho))  \mmember{}  Type
9.  t  :  J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}    {}\mrightarrow{}  T(f(rho))
10.  a  :  A(rho)
\mvdash{}  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}  .    ((w(f(rho))  J  1  (t  J  f))  =  (a  rho  f))  \mmember{}  \mBbbP{}


By

---

Latex:
RepeatFor  2  (((MemCD  THENW  Auto)  THENL  [Auto;    Id]))

---

Home Index