---

Step * 3 of Lemma unglue-term_wf

.....wf..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
7. u : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ A(a)
⊢ istype(∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((u I a a f) = (u J f(a)) ∈ A(f(a))))
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
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.  b  :  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}
7.  u  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:Gamma(I)  {}\mrightarrow{}  A(a)
\mvdash{}  istype(\mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:Gamma(I).    ((u  I  a  a  f)  =  (u  J  f(a))))


By

---

Latex:
Auto

---

Home Index