---

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


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. A : I@0:fset(ℕ) ⟶ I@0 ⟶ I ⟶ Type
4. x1 : I@0:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I@0 ⟶ a:I@0 ⟶ I ⟶ (A I@0 a) ⟶ (A J a ⋅ f)
5. ∀I@0:fset(ℕ). ∀a:I@0 ⟶ I. ∀u:A I@0 a.  ((x1 I@0 I@0 1 a u) = u ∈ (A I@0 a))
6. ∀I@0,J,K:fset(ℕ). ∀f:J ⟶ I@0. ∀g:K ⟶ J. ∀a:I@0 ⟶ I. ∀u:A I@0 a.
     ((x1 I@0 K f ⋅ g a u) = (x1 J K g a ⋅ f (x1 I@0 J f a u)) ∈ (A K a ⋅ f ⋅ g))
7. I@0 : fset(ℕ)
8. J : fset(ℕ)
9. f : J ⟶ I@0
10. a : I,psi(I@0)
11. x : A I@0 a
⊢ x1 I@0 J f a x ∈ A J f(a)
BY
{ (OnVar `a' (\h. (RWO "cubical-subset-I_cube" h THENA Auto))⋅ THEN RWO "cubical-subset-restriction" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  A  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  I@0  {}\mrightarrow{}  I  {}\mrightarrow{}  Type
4.  x1  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I@0  {}\mrightarrow{}  a:I@0  {}\mrightarrow{}  I  {}\mrightarrow{}  (A  I@0  a)  {}\mrightarrow{}  (A  J  a  \mcdot{}  f)
5.  \mforall{}I@0:fset(\mBbbN{}).  \mforall{}a:I@0  {}\mrightarrow{}  I.  \mforall{}u:A  I@0  a.    ((x1  I@0  I@0  1  a  u)  =  u)
6.  \mforall{}I@0,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:I@0  {}\mrightarrow{}  I.  \mforall{}u:A  I@0  a.
          ((x1  I@0  K  f  \mcdot{}  g  a  u)  =  (x1  J  K  g  a  \mcdot{}  f  (x1  I@0  J  f  a  u)))
7.  I@0  :  fset(\mBbbN{})
8.  J  :  fset(\mBbbN{})
9.  f  :  J  {}\mrightarrow{}  I@0
10.  a  :  I,psi(I@0)
11.  x  :  A  I@0  a
\mvdash{}  x1  I@0  J  f  a  x  \mmember{}  A  J  f(a)


By

---

Latex:
(OnVar  `a'  (\mbackslash{}h.  (RWO  "cubical-subset-I\_cube"  h  THENA  Auto))\mcdot{}
  THEN  RWO  "cubical-subset-restriction"  0
  THEN  Auto)

---

Home Index