---

Step * 2 of Lemma cubical-isect-elim_wf

.....set predicate..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. t : {X ⊢ _:⋂A B}
⊢ ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X.A(I).  ((cubical-isect-elim(t) I a a f) = (cubical-isect-elim(t) J f(a)) ∈ B(f(a)))
BY
{ (RepUR ``cubical-isect-elim cube-context-adjoin`` 0 THEN Auto THEN D -1 THEN Reduce 0 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. J : fset(ℕ)
8. f : J ⟶ I
9. alpha : X(I)
10. a1 : A(alpha)
⊢ (t I alpha I 1 <alpha, a1> f) = (t J f(alpha) J 1) ∈ B(<f(alpha), (a1 alpha f)>)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  t  :  \{X  \mvdash{}  \_:\mcap{}A  B\}
\mvdash{}  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:X.A(I).
        ((cubical-isect-elim(t)  I  a  a  f)  =  (cubical-isect-elim(t)  J  f(a)))


By

---

Latex:
(RepUR  ``cubical-isect-elim  cube-context-adjoin``  0  THEN  Auto  THEN  D  -1  THEN  Reduce  0  THEN  DVar  `t')

---

Home Index