---

Step * of Lemma csm-universe-type

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[K:fset(ℕ)]. ∀[f:K ⟶ I].
  ((universe-type(t;I;a))<f> = universe-type(t;K;f(a)) ∈ {formal-cube(K) ⊢ _})
BY
{ (Intros⋅
   THEN Unfold `universe-type` 0
   THEN (InstLemma `cubical-term-at-morph` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜X⌝;⌜c𝕌⌝;⌜t⌝;⌜I⌝;⌜a⌝;⌜K⌝;⌜f⌝]⋅ THENA Auto)
   THEN (RWO "cubical-universe-at" (-1) THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜fst(Z)⌝ ⌜{formal-cube(K) ⊢ _}⌝ (-1)⋅ THENA Auto)) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. a : X(I)
5. K : fset(ℕ)
6. f : K ⟶ I
7. (t(a) a f) = t(f(a)) ∈ (A:{formal-cube(K) ⊢ _} × formal-cube(K) ⊢ CompOp(A))
8. (fst((t(a) a f))) = (fst(t(f(a)))) ∈ {formal-cube(K) ⊢ _}
⊢ (fst(t(a)))<f> = (fst(t(f(a)))) ∈ {formal-cube(K) ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].  \mforall{}[K:fset(\mBbbN{})].  \mforall{}[f:K  {}\mrightarrow{}  I].
    ((universe-type(t;I;a))<f>  =  universe-type(t;K;f(a)))


By

---

Latex:
(Intros\mcdot{}
  THEN  Unfold  `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{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (RWO  "cubical-universe-at"  (-1)  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}fst(Z)\mkleeneclose{}  \mkleeneopen{}\{formal-cube(K)  \mvdash{}  \_\}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto))

---

Home Index