---

Step * 1 1 of Lemma universe-decode-restriction


1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. f : I ⟶ J
6. rho : X(J)
7. (t(rho) rho f) = t(f(rho)) ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
8. A : {formal-cube(I) ⊢ _}
9. x1 : formal-cube(I) ⊢ CompOp(A)
10. X ⊢' c𝕌
11. t(rho) ∈ A:{formal-cube(J) ⊢ _} × formal-cube(J) ⊢ CompOp(A)
12. A1 : {formal-cube(J) ⊢ _}
13. y1 : formal-cube(J) ⊢ CompOp(A1)
14. (A1)<f> = A ∈ {formal-cube(I) ⊢ _}
15. (y1)<f> = x1 ∈ formal-cube(I) ⊢ CompOp((A1)<f>)
⊢ A(1) = A1(f(1)) ∈ Type
BY
{ (ApFunToHypEquands `Z'  ⌜Z(1)⌝ ⌜Type⌝ (-2)⋅ THENA Auto) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. f : I ⟶ J
6. rho : X(J)
7. (t(rho) rho f) = t(f(rho)) ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))
8. A : {formal-cube(I) ⊢ _}
9. x1 : formal-cube(I) ⊢ CompOp(A)
10. X ⊢' c𝕌
11. t(rho) ∈ A:{formal-cube(J) ⊢ _} × formal-cube(J) ⊢ CompOp(A)
12. A1 : {formal-cube(J) ⊢ _}
13. y1 : formal-cube(J) ⊢ CompOp(A1)
14. (A1)<f> = A ∈ {formal-cube(I) ⊢ _}
15. (y1)<f> = x1 ∈ formal-cube(I) ⊢ CompOp((A1)<f>)
16. (A1)<f>(1) = A(1) ∈ Type
⊢ A(1) = A1(f(1)) ∈ Type

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  I  :  fset(\mBbbN{})
4.  J  :  fset(\mBbbN{})
5.  f  :  I  {}\mrightarrow{}  J
6.  rho  :  X(J)
7.  (t(rho)  rho  f)  =  t(f(rho))
8.  A  :  \{formal-cube(I)  \mvdash{}  \_\}
9.  x1  :  formal-cube(I)  \mvdash{}  CompOp(A)
10.  X  \mvdash{}'  c\mBbbU{}
11.  t(rho)  \mmember{}  A:\{formal-cube(J)  \mvdash{}  \_\}  \mtimes{}  formal-cube(J)  \mvdash{}  CompOp(A)
12.  A1  :  \{formal-cube(J)  \mvdash{}  \_\}
13.  y1  :  formal-cube(J)  \mvdash{}  CompOp(A1)
14.  (A1)<f>  =  A
15.  (y1)<f>  =  x1
\mvdash{}  A(1)  =  A1(f(1))


By

---

Latex:
(ApFunToHypEquands  `Z'    \mkleeneopen{}Z(1)\mkleeneclose{}  \mkleeneopen{}Type\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)

---

Home Index