---

Step * of Lemma sigma-box-fst_wf

∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}. ∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List.
∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i).
  (sigma-box-fst(bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i))
BY
{ ((UnivCD THENA Auto) THEN Unfold `sigma-box-fst` 0) }

1
1. X : CubicalSet
2. A : {X ⊢ _(Kan)}
3. B : {X.Kan-type(A) ⊢ _(Kan)}
4. I : Cname List
5. alpha : X(I)
6. J : nameset(I) List
7. x : nameset(I)
8. i : ℕ2
9. bx : A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)
⊢ map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i)

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_(Kan)\}.  \mforall{}B:\{X.Kan-type(A)  \mvdash{}  \_(Kan)\}.  \mforall{}I:Cname  List.  \mforall{}alpha:X(I).
\mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:A-open-box(X;\mSigma{}  Kan-type(A)  Kan-type(B);I;alpha;J;x;i).
    (sigma-box-fst(bx)  \mmember{}  A-open-box(X;Kan-type(A);I;alpha;J;x;i))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `sigma-box-fst`  0)

---

Home Index