---

Step * of Lemma unit-cube-cubical-type

∀[I:fset(ℕ)]
  ({formal-cube(I) ⊢ _} ~ {AF:A:L:fset(ℕ) ⟶ L ⟶ I ⟶ Type × (L:fset(ℕ)
                                                              ⟶ J:fset(ℕ)
                                                              ⟶ f:J ⟶ L
                                                              ⟶ a:L ⟶ I
                                                              ⟶ (A L a)
                                                              ⟶ (A J a ⋅ f))| 
                           let A,F = AF 
                           in (∀K:fset(ℕ). ∀a:K ⟶ I. ∀u:A K a.  ((F K K 1 a u) = u ∈ (A K a)))
                              ∧ (∀L,J,K:fset(ℕ). ∀f:J ⟶ L. ∀g:K ⟶ J. ∀a:L ⟶ I. ∀u:A L a.
                                   ((F L K f ⋅ g a u) = (F J K g a ⋅ f (F L J f a u)) ∈ (A K a ⋅ f ⋅ g)))} )
BY
{ PresheafMLTTInstance Obid: unit-set-presheaf-type⋅ }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})]
    (\{formal-cube(I)  \mvdash{}  \_\}  \msim{}  \{AF:A:L:fset(\mBbbN{})  {}\mrightarrow{}  L  {}\mrightarrow{}  I  {}\mrightarrow{}  Type  \mtimes{}  (L:fset(\mBbbN{})
                                                                                                                            {}\mrightarrow{}  J:fset(\mBbbN{})
                                                                                                                            {}\mrightarrow{}  f:J  {}\mrightarrow{}  L
                                                                                                                            {}\mrightarrow{}  a:L  {}\mrightarrow{}  I
                                                                                                                            {}\mrightarrow{}  (A  L  a)
                                                                                                                            {}\mrightarrow{}  (A  J  a  \mcdot{}  f))| 
                                                      let  A,F  =  AF 
                                                      in  (\mforall{}K:fset(\mBbbN{}).  \mforall{}a:K  {}\mrightarrow{}  I.  \mforall{}u:A  K  a.    ((F  K  K  1  a  u)  =  u))
                                                            \mwedge{}  (\mforall{}L,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  L.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:L  {}\mrightarrow{}  I.  \mforall{}u:A  L  a.
                                                                      ((F  L  K  f  \mcdot{}  g  a  u)  =  (F  J  K  g  a  \mcdot{}  f  (F  L  J  f  a  u))))\}  )


By

---

Latex:
PresheafMLTTInstance  Obid:  unit-set-presheaf-type\mcdot{}

---

Home Index