---

Step * 1 of Lemma cubical-isect-family_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. a : X(I)
6. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
7. J : fset(ℕ)
8. K : fset(ℕ)
9. f : J ⟶ I
10. g : K ⟶ J
11. u : A(f(a))
⊢ w K f ⋅ g ∈ B(g((f(a);u)))
BY
{ DoSubsume }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. a : X(I)
6. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
7. J : fset(ℕ)
8. K : fset(ℕ)
9. f : J ⟶ I
10. g : K ⟶ J
11. u : A(f(a))
⊢ w K f ⋅ g ∈ ⋂u:A(f ⋅ g(a)). B((f ⋅ g(a);u))

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. a : X(I)
6. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
7. J : fset(ℕ)
8. K : fset(ℕ)
9. f : J ⟶ I
10. g : K ⟶ J
11. u : A(f(a))
12. (w K f ⋅ g) = (w K f ⋅ g) ∈ (⋂u:A(f ⋅ g(a)). B((f ⋅ g(a);u)))
⊢ (⋂u:A(f ⋅ g(a)). B((f ⋅ g(a);u))) ⊆r B(g((f(a);u)))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  I  :  fset(\mBbbN{})
5.  a  :  X(I)
6.  w  :  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  (\mcap{}u:A(f(a)).  B((f(a);u)))
7.  J  :  fset(\mBbbN{})
8.  K  :  fset(\mBbbN{})
9.  f  :  J  {}\mrightarrow{}  I
10.  g  :  K  {}\mrightarrow{}  J
11.  u  :  A(f(a))
\mvdash{}  w  K  f  \mcdot{}  g  \mmember{}  B(g((f(a);u)))


By

---

Latex:
DoSubsume

---

Home Index