---

Step * 1 of Lemma glue-equations_wf

.....subterm..... T:t
1: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))} . ∀K:fset(ℕ). ∀g:K ⟶ J.
    ((t J f f(rho) g) = (t K f ⋅ g) ∈ T(f ⋅ g(rho))) ∈ ℙ
BY
{ (Auto THEN EAuto 2) }

---

Latex:

---

Latex:
.....subterm.....  T:t
1: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\}  .  \mforall{}K:fset(\mBbbN{}).  \mforall{}g:K  {}\mrightarrow{}  J.
        ((t  J  f  f(rho)  g)  =  (t  K  f  \mcdot{}  g))  \mmember{}  \mBbbP{}


By

---

Latex:
(Auto  THEN  EAuto  2)

---

Home Index