---

Step * of Lemma universe-decode-restriction

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}]. ∀[I,J:fset(ℕ)]. ∀[f:I ⟶ J]. ∀[rho:X(J)].
  (decode(t)(f(rho)) = universe-type(t;J;rho)(f(1)) ∈ Type)
BY
{ (Intros⋅
   THEN RepUR ``universe-decode universe-type`` 0
   THEN (InstLemma `cubical-term-at-morph` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜X⌝;⌜c𝕌⌝;⌜t⌝;⌜J⌝;⌜rho⌝;⌜I⌝;⌜f⌝]⋅ THENA Auto)
   THEN (RWO  "cubical-universe-at" (-1) THENA Auto)
   THEN DupHyp (-1)
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌜t(f(rho)) = xx ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))⌝⋅ THENA Auto)
         THEN Thin (-1)
         THEN D -1)
   THEN (((Assert X ⊢' c𝕌 BY Auto) THEN (Assert t(rho) ∈ c𝕌(rho) BY Auto))
         THEN (RWO "cubical-universe-at" (-1) THENA Auto)
         )
   THEN (GenConcl ⌜t(rho) = yy ∈ (A:{formal-cube(J) ⊢ _} × formal-cube(J) ⊢ CompOp(A))⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN Reduce 0) }

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)
⊢ ((<A1, y1> rho f) = <A, x1> ∈ (A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A))) ⇒ (A(1) = A1(f(1)) ∈ Type)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:I  {}\mrightarrow{}  J].  \mforall{}[rho:X(J)].
    (decode(t)(f(rho))  =  universe-type(t;J;rho)(f(1)))


By

---

Latex:
(Intros\mcdot{}
  THEN  RepUR  ``universe-decode  universe-type``  0
  THEN  (InstLemma  `cubical-term-at-morph`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}rho\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (RWO    "cubical-universe-at"  (-1)  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}t(f(rho))  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1)
  THEN  (((Assert  X  \mvdash{}'  c\mBbbU{}  BY  Auto)  THEN  (Assert  t(rho)  \mmember{}  c\mBbbU{}(rho)  BY  Auto))
              THEN  (RWO  "cubical-universe-at"  (-1)  THENA  Auto)
              )
  THEN  (GenConcl  \mkleeneopen{}t(rho)  =  yy\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index