---

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

.....wf..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
6. u : I@0:fset(ℕ) ⟶ a:I,psi(I@0) ⟶ T(a)
⊢ ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I,psi(I@0).  ((u I@0 a a f) = (u J f(a)) ∈ T(f(a))) ∈ Type
BY
{ ((Assert ⌜{formal-cube(I) ⊢ _} ⊆r {I,psi ⊢ _}⌝⋅ THENA Auto)
   THEN MoveToConcl (-2)
   THEN (GenConcl ⌜T = X ∈ {I,psi ⊢ _}⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜I,psi = Y ∈ CubicalSet⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  T  :  \{formal-cube(I)  \mvdash{}  \_\}
4.  x  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  a:formal-cube(I)(I@0)  {}\mrightarrow{}  T(a)
5.  \mforall{}I@0,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}a:formal-cube(I)(I@0).    ((x  I@0  a  a  f)  =  (x  J  f(a)))
6.  u  :  I@0:fset(\mBbbN{})  {}\mrightarrow{}  a:I,psi(I@0)  {}\mrightarrow{}  T(a)
\mvdash{}  \mforall{}I@0,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I@0.  \mforall{}a:I,psi(I@0).    ((u  I@0  a  a  f)  =  (u  J  f(a)))  \mmember{}  Type


By

---

Latex:
((Assert  \mkleeneopen{}\{formal-cube(I)  \mvdash{}  \_\}  \msubseteq{}r  \{I,psi  \mvdash{}  \_\}\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  (GenConcl  \mkleeneopen{}T  =  X\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}I,psi  =  Y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index