---

Step * 1 of Lemma universe-comp-op_wf


1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
⊢ compOp(t) ∈ I:fset(ℕ)
  ⟶ i:{i:ℕ| ¬i ∈ I} 
  ⟶ rho:X(I+i)
  ⟶ phi:𝔽(I)
  ⟶ u:{I+i,s(phi) ⊢ _:(decode(t))<rho> o iota}
  ⟶ cubical-path-0(X;decode(t);I;i;rho;phi;u)
  ⟶ cubical-path-1(X;decode(t);I;i;rho;phi;u)
BY
{ ((Unfold `universe-comp-op` 0 THEN RepeatFor 3 ((MemCD THENA Auto)))
   THEN (Assert t(rho) ∈ c𝕌(rho) BY
               (MemCD THEN Auto))
   THEN (RWO "cubical-universe-at" (-1) THENA Auto)
   THEN (Assert snd(t(rho)) ∈ formal-cube(I+i) ⊢ CompOp(fst(t(rho))) BY
               Auto)
   THEN Unfold `composition-op` -1) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. i : {i:ℕ| ¬i ∈ I} 
5. rho : X(I+i)
6. t(rho) ∈ A:{formal-cube(I+i) ⊢ _} × formal-cube(I+i) ⊢ CompOp(A)
7. snd(t(rho)) ∈ {comp:I@0:fset(ℕ)
                  ⟶ i@0:{i:ℕ| ¬i ∈ I@0} 
                  ⟶ rho@0:formal-cube(I+i)(I@0+i@0)
                  ⟶ phi:𝔽(I@0)
                  ⟶ u:{I@0+i@0,s(phi) ⊢ _:(fst(t(rho)))<rho@0> o iota}
                  ⟶ cubical-path-0(formal-cube(I+i);fst(t(rho));I@0;i@0;rho@0;phi;u)
                  ⟶ cubical-path-1(formal-cube(I+i);fst(t(rho));I@0;i@0;rho@0;phi;u)| 
                  composition-uniformity(formal-cube(I+i);fst(t(rho));comp)} 
⊢ (snd(t(rho))) I i 1 ∈ phi:𝔽(I)
  ⟶ u:{I+i,s(phi) ⊢ _:(decode(t))<rho> o iota}
  ⟶ cubical-path-0(X;decode(t);I;i;rho;phi;u)
  ⟶ cubical-path-1(X;decode(t);I;i;rho;phi;u)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
\mvdash{}  compOp(t)  \mmember{}  I:fset(\mBbbN{})
    {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
    {}\mrightarrow{}  rho:X(I+i)
    {}\mrightarrow{}  phi:\mBbbF{}(I)
    {}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(decode(t))<rho>  o  iota\}
    {}\mrightarrow{}  cubical-path-0(X;decode(t);I;i;rho;phi;u)
    {}\mrightarrow{}  cubical-path-1(X;decode(t);I;i;rho;phi;u)


By

---

Latex:
((Unfold  `universe-comp-op`  0  THEN  RepeatFor  3  ((MemCD  THENA  Auto)))
  THEN  (Assert  t(rho)  \mmember{}  c\mBbbU{}(rho)  BY
                          (MemCD  THEN  Auto))
  THEN  (RWO  "cubical-universe-at"  (-1)  THENA  Auto)
  THEN  (Assert  snd(t(rho))  \mmember{}  formal-cube(I+i)  \mvdash{}  CompOp(fst(t(rho)))  BY
                          Auto)
  THEN  Unfold  `composition-op`  -1)

---

Home Index