---

Step * of Lemma universe-decode_wf

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}].  X ⊢ decode(t)
BY
{ ((Intros
    THEN (Assert ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌') BY
                (RepUR ``cubical-term-at cubical-universe closed-type-to-type`` 0 THEN Auto))
    THEN (InstLemma `cubical-term-at_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜X⌝;⌜c𝕌⌝]⋅ THENA Auto))
   THEN (MemTypeCD THENW Auto)
   THEN RepUR ``universe-decode`` 0) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌')
4. ∀[u:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ c𝕌(a))
⊢ <λI,a. fst(t(a))(1), λI,J,f,a,x. (x 1 f)> ∈ A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ)
                                                              ⟶ J:fset(ℕ)
                                                              ⟶ f:J ⟶ I
                                                              ⟶ a:X(I)
                                                              ⟶ (A I a)
                                                              ⟶ (A J f(a)))

2
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌')
4. ∀[u:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ c𝕌(a))
⊢ (∀I:fset(ℕ). ∀a:X(I). ∀u:fst(t(a))(1).  ((u 1 1) = u ∈ fst(t(a))(1)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:fst(t(a))(1).  ((u 1 f ⋅ g) = ((u 1 f) 1 g) ∈ fst(t(f ⋅ g(a)))(1)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].    X  \mvdash{}  decode(t)


By

---

Latex:
((Intros
    THEN  (Assert  \mforall{}I:fset(\mBbbN{}).  \mforall{}a:Top.    (c\mBbbU{}(a)  \mmember{}  \mBbbU{}')  BY
                            (RepUR  ``cubical-term-at  cubical-universe  closed-type-to-type``  0  THEN  Auto))
    THEN  (InstLemma  `cubical-term-at\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepUR  ``universe-decode``  0)

---

Home Index