---

Step * 1 2 4 1 1 2 2 5 2 1 1 1 1 2 2 1 of Lemma csm-glue-type


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. Z : CubicalSet{j}
7. s : Z j⟶ Gamma
8. (phi)s ∈ {Z ⊢ _:𝔽}
9. Z, (phi)s j⊢
10. s ∈ Z, (phi)s j⟶ Gamma, phi
11. I : fset(ℕ)
12. x : Z(I)
13. ¬((phi)s(x) = 1 ∈ Point(face_lattice(I)))
14. t1 : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f((s)x)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f((s)x))
15. t2 : A((s)x)
16. J : fset(ℕ)
17. f : {f:J ⟶ I| phi(f((s)x)) = 1 ∈ Point(face_lattice(J))} 
18. A(1(f((s)x))) = A(f((s)x)) ∈ Type
19. w(f((s)x)) = w((s)f(x)) ∈ (T ⟶ A)(f((s)x))
20. f((s)x) ∈ Gamma, phi(J)
⊢ istype((T ⟶ A)(f((s)x)))
BY
{ Auto }

---

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.  Z  :  CubicalSet\{j\}
7.  s  :  Z  j{}\mrightarrow{}  Gamma
8.  (phi)s  \mmember{}  \{Z  \mvdash{}  \_:\mBbbF{}\}
9.  Z,  (phi)s  j\mvdash{}
10.  s  \mmember{}  Z,  (phi)s  j{}\mrightarrow{}  Gamma,  phi
11.  I  :  fset(\mBbbN{})
12.  x  :  Z(I)
13.  \mneg{}((phi)s(x)  =  1)
14.  t1  :  J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f((s)x))  =  1\}    {}\mrightarrow{}  T(f((s)x))
15.  t2  :  A((s)x)
16.  J  :  fset(\mBbbN{})
17.  f  :  \{f:J  {}\mrightarrow{}  I|  phi(f((s)x))  =  1\} 
18.  A(1(f((s)x)))  =  A(f((s)x))
19.  w(f((s)x))  =  w((s)f(x))
20.  f((s)x)  \mmember{}  Gamma,  phi(J)
\mvdash{}  istype((T  {}\mrightarrow{}  A)(f((s)x)))


By

---

Latex:
Auto

---

Home Index