---

Step * 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)
⊢ ((<A1, y1> rho f) = <A, x1> ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))) ⇒ (A(1) = A1(f(1)) ∈ Type)
BY
{ ((RepUR ``cubical-universe closed-cubical-universe`` 0 THEN RepUR ``closed-type-to-type csm-fibrant-type`` 0)
   THEN (D 0 THENA (Auto THEN RepUR ``formal-cube`` 0 THEN Auto))
   THEN (EqHD  (-1) THENA Auto)
   THEN All Reduce) }

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>)
⊢ 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)
\mvdash{}  ((<A1,  y1>  rho  f)  =  <A,  x1>)  {}\mRightarrow{}  (A(1)  =  A1(f(1)))


By

---

Latex:
((RepUR  ``cubical-universe  closed-cubical-universe``  0
    THEN  RepUR  ``closed-type-to-type  csm-fibrant-type``  0
    )
  THEN  (D  0  THENA  (Auto  THEN  RepUR  ``formal-cube``  0  THEN  Auto))
  THEN  (EqHD    (-1)  THENA  Auto)
  THEN  All  Reduce)

---

Home Index