---

Step * of Lemma composition-op-universe-sq

No Annotations
∀[G:Top]
  (G ⊢ CompOp(c𝕌) ~ {comp:I:fset(ℕ)
                     ⟶ i:{i:ℕ| ¬i ∈ I} 
                     ⟶ rho:G(I+i)
                     ⟶ phi:𝔽(I)
                     ⟶ u:{I+i,s(phi) ⊢ _:c𝕌}
                     ⟶ {a0:FibrantType(formal-cube(I))| 
                         ∀J:fset(ℕ). ∀f:I,phi(J).
                           (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>;a0)
                           = u((i0) ⋅ f)
                           ∈ FibrantType(formal-cube(J)))} 
                     ⟶ {a1:FibrantType(formal-cube(I))| 
                         ∀J:fset(ℕ). ∀f:I,phi(J).
                           (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>;a1)
                           = u((i1) ⋅ f)
                           ∈ FibrantType(formal-cube(J)))} | 
                     ∀I,J:fset(ℕ). ∀i:{i:ℕ| ¬i ∈ I} . ∀j:{j:ℕ| ¬j ∈ J} . ∀g:J ⟶ I. ∀rho:G(I+i). ∀phi:𝔽(I).
                     ∀u:{I+i,s(phi) ⊢ _:c𝕌}. ∀a0:{a0:FibrantType(formal-cube(I))| 
                                                  ∀J:fset(ℕ). ∀f:I,phi(J).
                                                    (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>;a0)
                                                    = u((i0) ⋅ f)
                                                    ∈ FibrantType(formal-cube(J)))} .
                       (csm-fibrant-type(formal-cube(I);formal-cube(J);<g>;comp I i rho phi u a0)
                       = (comp J j g,i=j(rho) g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) 
                          csm-fibrant-type(formal-cube(I);formal-cube(J);<g>;a0))
                       ∈ FibrantType(formal-cube(J)))} )
BY
{ (Intro
   THEN RepUR ``composition-op composition-uniformity`` 0
   THEN RepUR ``cubical-path-0 cubical-path-1`` 0
   THEN RepUR ``cubical-path-condition cubical-path-condition\'`` 0
   THEN (RWO  "csm-cubical-universe cubical-universe-at" 0 THENA Auto)
   THEN Fold `fibrant-type` 0
   THEN RWO "cubical-universe-ap-morph" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:Top]
    (G  \mvdash{}  CompOp(c\mBbbU{})  \msim{}  \{comp:I:fset(\mBbbN{})
                                          {}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
                                          {}\mrightarrow{}  rho:G(I+i)
                                          {}\mrightarrow{}  phi:\mBbbF{}(I)
                                          {}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:c\mBbbU{}\}
                                          {}\mrightarrow{}  \{a0:FibrantType(formal-cube(I))| 
                                                  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).
                                                      (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>a0)  =  u((i0)  \mcdot{}  f))\} 
                                          {}\mrightarrow{}  \{a1:FibrantType(formal-cube(I))| 
                                                  \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).
                                                      (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>a1)  =  u((i1)  \mcdot{}  f))\}  |\000C 
                                          \mforall{}I,J:fset(\mBbbN{}).  \mforall{}i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  .  \mforall{}j:\{j:\mBbbN{}|  \mneg{}j  \mmember{}  J\}  .  \mforall{}g:J  {}\mrightarrow{}  I.  \mforall{}rho:G(I+i).
                                          \mforall{}phi:\mBbbF{}(I).  \mforall{}u:\{I+i,s(phi)  \mvdash{}  \_:c\mBbbU{}\}.
                                          \mforall{}a0:\{a0:FibrantType(formal-cube(I))| 
                                                    \mforall{}J:fset(\mBbbN{}).  \mforall{}f:I,phi(J).
                                                        (csm-fibrant-type(formal-cube(I);formal-cube(J);<f>a0)  =  u((i0)  \mcdot{}  f))\}  \000C.
                                              (csm-fibrant-type(formal-cube(I);formal-cube(J);<g>comp  I  i  rho  phi  u  a0)
                                              =  (comp  J  j  g,i=j(rho)  g(phi)  (u)subset-trans(I+i;J+j;g,i=j;s(phi)) 
                                                    csm-fibrant-type(formal-cube(I);formal-cube(J);<g>a0)))\}  )


By

---

Latex:
(Intro
  THEN  RepUR  ``composition-op  composition-uniformity``  0
  THEN  RepUR  ``cubical-path-0  cubical-path-1``  0
  THEN  RepUR  ``cubical-path-condition  cubical-path-condition\mbackslash{}'``  0
  THEN  (RWO    "csm-cubical-universe  cubical-universe-at"  0  THENA  Auto)
  THEN  Fold  `fibrant-type`  0
  THEN  RWO  "cubical-universe-ap-morph"  0
  THEN  Auto)

---

Home Index