---

Step * 1 of Lemma cubical-isect-elim_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. t : {X ⊢ _:⋂A B}
⊢ cubical-isect-elim(t) ∈ I:fset(ℕ) ⟶ a:X.A(I) ⟶ B(a)
BY
{ ((Unfold `cubical-isect-elim` 0 THEN RepeatFor 2 ((MemCD THENA Auto))) THEN DVar `t') }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. t : I:fset(ℕ) ⟶ a:X(I) ⟶ ⋂A B(a)
5. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((t I a a f) = (t J f(a)) ∈ ⋂A B(f(a)))
6. I : fset(ℕ)
7. a : X.A(I)
⊢ t I (fst(a)) I 1 ∈ B(a)

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  t  :  \{X  \mvdash{}  \_:\mcap{}A  B\}
\mvdash{}  cubical-isect-elim(t)  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:X.A(I)  {}\mrightarrow{}  B(a)


By

---

Latex:
((Unfold  `cubical-isect-elim`  0  THEN  RepeatFor  2  ((MemCD  THENA  Auto)))  THEN  DVar  `t')

---

Home Index