---

Step * 3 of Lemma cubical-type-subtype-cubical-subset


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. A : I@0:fset(ℕ) ⟶ formal-cube(I)(I@0) ⟶ Type
4. x1 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:formal-cube(I)(I@0) ⟶ (A I@0 a) ⟶ (A J f(a))
5. (∀I@0:fset(ℕ). ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.  ((x1 I@0 I@0 1 a u) = u ∈ (A I@0 a)))
∧ (∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:formal-cube(I)(I@0). ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g f(a) (x1 I@0 J f a u)) ∈ (A K f ⋅ g(a))))
6. A1 : I@0:fset(ℕ) ⟶ I,psi(I@0) ⟶ Type
7. A2 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:I,psi(I@0) ⟶ (A1 I@0 a) ⟶ (A1 J f(a))
⊢ (∀I@0:fset(ℕ). ∀a:I,psi(I@0). ∀u:A1 I@0 a.  ((A2 I@0 I@0 1 a u) = u ∈ (A1 I@0 a)))
  ∧ (∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:I,psi(I@0). ∀u:A1 I@0 a.
       ((A2 I@0 K f ⋅ g a u) = (A2 J K g f(a) (A2 I@0 J f a u)) ∈ (A1 K f ⋅ g(a)))) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  A  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  formal-cube(I)(I@0)  {}\mrightarrow{}  Type
4.  x1  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I@0  {}\mrightarrow{}  a:formal-cube(I)(I@0)  {}\mrightarrow{}  (A  I@0  a)  {}\mrightarrow{}  (A  J  f(a))
5.  (\mforall{}I@0:fset(\mBbbN{}).  \mforall{}a:formal-cube(I)(I@0).  \mforall{}u:A  I@0  a.    ((x1  I@0  I@0  1  a  u)  =  u))
\mwedge{}  (\mforall{}I@0,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:formal-cube(I)(I@0).  \mforall{}u:A  I@0  a.
          ((x1  I@0  K  f  \mcdot{}  g  a  u)  =  (x1  J  K  g  f(a)  (x1  I@0  J  f  a  u))))
6.  A1  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  I,psi(I@0)  {}\mrightarrow{}  Type
7.  A2  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I@0  {}\mrightarrow{}  a:I,psi(I@0)  {}\mrightarrow{}  (A1  I@0  a)  {}\mrightarrow{}  (A1  J  f(a))
\mvdash{}  (\mforall{}I@0:fset(\mBbbN{}).  \mforall{}a:I,psi(I@0).  \mforall{}u:A1  I@0  a.    ((A2  I@0  I@0  1  a  u)  =  u))
    \mwedge{}  (\mforall{}I@0,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:I,psi(I@0).  \mforall{}u:A1  I@0  a.
              ((A2  I@0  K  f  \mcdot{}  g  a  u)  =  (A2  J  K  g  f(a)  (A2  I@0  J  f  a  u))))  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index