---

Step * of Lemma cubical-universe-I-cube

∀[I:Cname List]
  (c𝕌(I) ~ {p:AF:{AF:A:L:(Cname List) ⟶ name-morph(I;L) ⟶ Type × (L:(Cname List)
                                                                   ⟶ J:(Cname List)
                                                                   ⟶ f:name-morph(L;J)
                                                                   ⟶ a:name-morph(I;L)
                                                                   ⟶ (A L a)
                                                                   ⟶ (A J (a o f)))| 
                  let A,F = AF 
                  in (∀K:Cname List. ∀a:name-morph(I;K). ∀u:A K a.  ((F K K 1 a u) = u ∈ (A K a)))
                     ∧ (∀L,J,K:Cname List. ∀f:name-morph(L;J). ∀g:name-morph(J;K). ∀a:name-morph(I;L). ∀u:A L a.
                          ((F L K (f o g) a u) = (F J K g (a o f) (F L J f a u)) ∈ (A K (a o (f o g)))))} 
            × (L:(Cname List)
              ⟶ f:name-morph(I;L)
              ⟶ J:(nameset(L) List)
              ⟶ x:nameset(L)
              ⟶ i:ℕ2
              ⟶ A-open-box(unit-cube(I);AF;L;f;J;x;i)
              ⟶ ((fst(AF)) L f))| 
            let AF,filler = p 
            in Kan-A-filler(unit-cube(I);AF;filler) ∧ uniform-Kan-A-filler(unit-cube(I);AF;filler)} )
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``I-cube cubical-universe functor-ob Kan-cubical-type`` 0
   THEN (RWO "unit-cube-cubical-type" 0 THEN RepUR ``unit-cube cubical-type-at`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Cname  List]
    (c\mBbbU{}(I)  \msim{}  \{p:AF:\{AF:A:L:(Cname  List)  {}\mrightarrow{}  name-morph(I;L)  {}\mrightarrow{}  Type  \mtimes{}  (L:(Cname  List)
                                                                                                                                      {}\mrightarrow{}  J:(Cname  List)
                                                                                                                                      {}\mrightarrow{}  f:name-morph(L;J)
                                                                                                                                      {}\mrightarrow{}  a:name-morph(I;L)
                                                                                                                                      {}\mrightarrow{}  (A  L  a)
                                                                                                                                      {}\mrightarrow{}  (A  J  (a  o  f)))| 
                                    let  A,F  =  AF 
                                    in  (\mforall{}K:Cname  List.  \mforall{}a:name-morph(I;K).  \mforall{}u:A  K  a.    ((F  K  K  1  a  u)  =  u))
                                          \mwedge{}  (\mforall{}L,J,K:Cname  List.  \mforall{}f:name-morph(L;J).  \mforall{}g:name-morph(J;K).
                                                \mforall{}a:name-morph(I;L).  \mforall{}u:A  L  a.
                                                    ((F  L  K  (f  o  g)  a  u)  =  (F  J  K  g  (a  o  f)  (F  L  J  f  a  u))))\} 
                        \mtimes{}  (L:(Cname  List)
                            {}\mrightarrow{}  f:name-morph(I;L)
                            {}\mrightarrow{}  J:(nameset(L)  List)
                            {}\mrightarrow{}  x:nameset(L)
                            {}\mrightarrow{}  i:\mBbbN{}2
                            {}\mrightarrow{}  A-open-box(unit-cube(I);AF;L;f;J;x;i)
                            {}\mrightarrow{}  ((fst(AF))  L  f))| 
                        let  AF,filler  =  p 
                        in  Kan-A-filler(unit-cube(I);AF;filler)  \mwedge{}  uniform-Kan-A-filler(unit-cube(I);AF;filler)\}  \000C)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RepUR  ``I-cube  cubical-universe  functor-ob  Kan-cubical-type``  0
  THEN  (RWO  "unit-cube-cubical-type"  0  THEN  RepUR  ``unit-cube  cubical-type-at``  0)
  THEN  Auto)

---

Home Index