---

Step * of Lemma cubical-isect-elim_wf

∀[X:⊢]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[t:{X ⊢ _:⋂A B}].  (cubical-isect-elim(t) ∈ {X.A ⊢ _:B})
BY
{ (Intros THEN (MemTypeCD THENW Auto)) }

1
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)

2
.....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)))

---

Latex:

---

Latex:
\mforall{}[X:\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[t:\{X  \mvdash{}  \_:\mcap{}A  B\}].    (cubical-isect-elim(t)  \mmember{}  \{X.A  \mvdash{}  \_:B\})


By

---

Latex:
(Intros  THEN  (MemTypeCD  THENW  Auto))

---

Home Index