---

Step * of Lemma compU_wf

No Annotations
∀[G:j⊢]. (compU() ∈ G ⊢ Compositon'(c𝕌))
BY
{ (Auto
   THEN MemTypeCD
   THEN Auto
   THEN RepeatFor 5 ((D 0 THENA Auto))
   THEN (RWO  "csm-cubical-universe" 0 THENA Auto)
   THEN (InstLemma `cubical-term_wf` [parm{j};⌜parm{i'}⌝;⌜H, phi.𝕀⌝;⌜c𝕌⌝]⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Unfold `constrained-cubical-term` 0
   THEN (RWO  "csm-cubical-universe" 0 THENA Auto)
   THEN (InstLemma `cubical-term_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜H⌝;⌜c𝕌⌝]⋅ THENA Auto)
   THEN (InstLemma `cubical-term_wf` [parm{j};⌜parm{i'}⌝;⌜H, phi⌝;⌜c𝕌⌝]⋅ THENA Auto)) }

1
1. G : CubicalSet{j}
2. H : CubicalSet{j}
3. K : CubicalSet{j}
4. tau : K j⟶ H
5. sigma : H.𝕀 j⟶ G
6. phi : {H ⊢ _:𝔽}
7. {H, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
8. u : {H, phi.𝕀 ⊢ _:c𝕌}
9. {H ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
10. {H, phi ⊢ _:c𝕌} ∈ 𝕌{[i' | j']}
⊢ ∀a0:{a:{H ⊢ _:c𝕌}| (u)[0(𝕀)] = a ∈ {H, phi ⊢ _:c𝕌}} 
    ((compU() H sigma phi u a0)tau
    = (compU() K sigma o tau+ (phi)tau (u)tau+ (a0)tau)
    ∈ {a:{K ⊢ _:(c𝕌)tau}| ((u)[1(𝕀)])tau = a ∈ {K, (phi)tau ⊢ _:(c𝕌)tau}} )

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  (compU()  \mmember{}  G  \mvdash{}  Compositon'(c\mBbbU{}))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepeatFor  5  ((D  0  THENA  Auto))
  THEN  (RWO    "csm-cubical-universe"  0  THENA  Auto)
  THEN  (InstLemma  `cubical-term\_wf`  [parm\{j\};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}H,  phi.\mBbbI{}\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `constrained-cubical-term`  0
  THEN  (RWO    "csm-cubical-universe"  0  THENA  Auto)
  THEN  (InstLemma  `cubical-term\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `cubical-term\_wf`  [parm\{j\};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}H,  phi\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index