---

Step * 1 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)
= <λ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))))
BY
{ ((Subst' universe-type(t;I;rho) ~ <fst(universe-type(t;I;rho)), snd(universe-type(t;I;rho))> 0
    THENA ((GenConclTerm ⌜universe-type(t;I;rho)⌝⋅ THENA Auto) THEN RepeatFor 2 (DVar `v') THEN Reduce 0 THEN Auto)
    )
THENM (EqCD THENA Auto)
) }

1
.....subterm..... T:t
1:n
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. rho : X(I)
⊢ (fst(universe-type(t;I;rho))) = (λJ,a. fst(t(a(rho)))(1)) ∈ (I1:fset(ℕ) ⟶ formal-cube(I)(I1) ⟶ Type)

2
.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. rho : X(I)
⊢ (snd(universe-type(t;I;rho)))
= (λK,J,f,a,u. (u 1 f))
∈ (I1:fset(ℕ)
  ⟶ J:fset(ℕ)
  ⟶ f:J ⟶ I1
  ⟶ a:formal-cube(I)(I1)
  ⟶ ((fst(universe-type(t;I;rho))) I1 a)
  ⟶ ((fst(universe-type(t;I;rho))) 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)  =  <\mlambda{}J,a.  fst(t(a(rho)))(1),  \mlambda{}K,J,f,a,u.  (u  1  f)>


By

---

Latex:
((Subst'  universe-type(t;I;rho)  \msim{}  <fst(universe-type(t;I;rho)),  snd(universe-type(t;I;rho))>  0
    THENA  ((GenConclTerm  \mkleeneopen{}universe-type(t;I;rho)\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  RepeatFor  2  (DVar  `v')
                  THEN  Reduce  0
                  THEN  Auto)
    )
THENM  (EqCD  THENA  Auto)
)

---

Home Index