---

Step * of Lemma universe-encode_wf

No Annotations
∀[G:j⊢]. ∀[T:{G ⊢ _}]. ∀[cT:G ⊢ CompOp(T)].  (encode(T;cT) ∈ {G ⊢ _:c𝕌})
BY
{ (Intros
   THEN Unhide
   THEN (Assert G ⊢' c𝕌 BY
               Auto)
   THEN (MemTypeCD THENW Auto)
   THEN (RepeatFor 2 ((FunExt THENA Auto)) ORELSE Intros)
   THEN RepUR ``universe-encode`` 0
   THEN (RWO "cubical-universe-at" 0 THENA Auto)) }

1
1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. a : G(I)
⊢ <(T)<a>, (cT)<a>> ∈ A:{formal-cube(I) ⊢ _} × formal-cube(I) ⊢ CompOp(A)

2
1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : G(I)
⊢ (<(T)<a>, (cT)<a>> a f) = <(T)<f(a)>, (cT)<f(a)>> ∈ (A:{formal-cube(J) ⊢ _} × formal-cube(J) ⊢ CompOp(A))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[T:\{G  \mvdash{}  \_\}].  \mforall{}[cT:G  \mvdash{}  CompOp(T)].    (encode(T;cT)  \mmember{}  \{G  \mvdash{}  \_:c\mBbbU{}\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  G  \mvdash{}'  c\mBbbU{}  BY
                          Auto)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  (RepeatFor  2  ((FunExt  THENA  Auto))  ORELSE  Intros)
  THEN  RepUR  ``universe-encode``  0
  THEN  (RWO  "cubical-universe-at"  0  THENA  Auto))

---

Home Index