---

Step * 1 of Lemma fst-transprt-sigma

.....assertion..... 
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
⊢ pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}
BY
{ MemTypeCD⋅ }

1
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
⊢ pr.1 ∈ {X ⊢ _:(A)[0(𝕀)]}

2
.....set predicate..... 
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
⊢ partial-term-0(X;discr(⋅).1) = pr.1 ∈ {X, 0(𝔽) ⊢ _:(A)[0(𝕀)]}

3
.....wf..... 
1. X : CubicalSet{j}
2. A : {X.𝕀 ⊢ _}
3. B : {X.𝕀.A ⊢ _}
4. cA : X.𝕀 +⊢ Compositon(A)
5. cB : X.𝕀.A +⊢ Compositon(B)
6. pr : {X ⊢ _:(Σ A B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
8. a : {X ⊢ _:(A)[0(𝕀)]}
⊢ istype(partial-term-0(X;discr(⋅).1) = a ∈ {X, 0(𝔽) ⊢ _:(A)[0(𝕀)]})

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet\{j\}
2.  A  :  \{X.\mBbbI{}  \mvdash{}  \_\}
3.  B  :  \{X.\mBbbI{}.A  \mvdash{}  \_\}
4.  cA  :  X.\mBbbI{}  +\mvdash{}  Compositon(A)
5.  cB  :  X.\mBbbI{}.A  +\mvdash{}  Compositon(B)
6.  pr  :  \{X  \mvdash{}  \_:(\mSigma{}  A  B)[0(\mBbbI{})]\}
7.  (cA)1(X.\mBbbI{})  \mmember{}  X.\mBbbI{}  +\mvdash{}  Compositon(A)
\mvdash{}  pr.1  \mmember{}  \{X  \mvdash{}  \_:(A)[0(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  discr(\mcdot{}).1[0]]\}


By

---

Latex:
MemTypeCD\mcdot{}

---

Home Index