---

Step * 1 of Lemma universe-decode-type


1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. rho : X(I)
⊢ universe-type(t;I;rho)
= (decode(t))<rho>
∈ (A:I1:fset(ℕ) ⟶ formal-cube(I)(I1) ⟶ Type × (I1:fset(ℕ)
                                                ⟶ J:fset(ℕ)
                                                ⟶ f:J ⟶ I1
                                                ⟶ a:formal-cube(I)(I1)
                                                ⟶ (A I1 a)
                                                ⟶ (A J f(a))))
BY
{ (Subst' (decode(t))<rho> ~ <λJ,a. fst(t(a(rho)))(1), λK,J,f,a,u. (u 1 f)> 0
   THENA (RepUR ``universe-decode csm-ap-type`` 0
          THEN RepUR ``context-map csm-ap-term csm-ap cubical-term-at cubical-type-at`` 0
          THEN (Unfold `functor-arrow` 0 THEN Fold `cube-set-restriction` 0)
          THEN Fold `cubical-term-at` 0
          THEN Auto)
   ) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. rho : X(I)
⊢ universe-type(t;I;rho)
= <λJ,a. fst(t(a(rho)))(1), λK,J,f,a,u. (u 1 f)>
∈ (A:I1:fset(ℕ) ⟶ formal-cube(I)(I1) ⟶ Type × (I1:fset(ℕ)
                                                ⟶ J:fset(ℕ)
                                                ⟶ f:J ⟶ I1
                                                ⟶ a:formal-cube(I)(I1)
                                                ⟶ (A I1 a)
                                                ⟶ (A J f(a))))

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  I  :  fset(\mBbbN{})
4.  rho  :  X(I)
\mvdash{}  universe-type(t;I;rho)  =  (decode(t))<rho>


By

---

Latex:
(Subst'  (decode(t))<rho>  \msim{}  <\mlambda{}J,a.  fst(t(a(rho)))(1),  \mlambda{}K,J,f,a,u.  (u  1  f)>  0
  THENA  (RepUR  ``universe-decode  csm-ap-type``  0
                THEN  RepUR  ``context-map  csm-ap-term  csm-ap  cubical-term-at  cubical-type-at``  0
                THEN  (Unfold  `functor-arrow`  0  THEN  Fold  `cube-set-restriction`  0)
                THEN  Fold  `cubical-term-at`  0
                THEN  Auto)
  )

---

Home Index