---

Step * 2 of Lemma fst-transprt-sigma


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. pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}
9. ∀[u:{X.𝕀, 0(𝔽) ⊢ _:A}]. ∀[a0:{X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ u[0]]}]. ∀[cT:X.𝕀 ⊢ Compositon(A)].
     ((fill cT [0(𝔽) ⊢→ u] a0)[1(𝕀)] = comp cT [0(𝔽) ⊢→ u] a0 ∈ {X ⊢ _:(A)[1(𝕀)]})
10. (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}
⊢ (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = transprt(X;cA;pr.1) ∈ {X ⊢ _:(A)[1(𝕀)]}
BY
{ (Thin (-2)
   THEN NthHypEqGen (-1)
   THEN EqCDA
   THEN Assert ⌜transprt(X;(cA)1(X.𝕀);pr.1) = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}⌝⋅) }

1
.....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)
8. pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}
9. (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}
⊢ transprt(X;(cA)1(X.𝕀);pr.1) = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}

2
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. pr.1 ∈ {X ⊢ _:(A)[0(𝕀)][0(𝔽) |⟶ discr(⋅).1[0]]}
9. (fill (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1)[1(𝕀)] = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}
10. transprt(X;(cA)1(X.𝕀);pr.1) = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}
⊢ transprt(X;cA;pr.1) = comp (cA)1(X.𝕀) [0(𝔽) ⊢→ discr(⋅).1] pr.1 ∈ {X ⊢ _:(A)[1(𝕀)]}

---

Latex:

---

Latex:

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)
8.  pr.1  \mmember{}  \{X  \mvdash{}  \_:(A)[0(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  discr(\mcdot{}).1[0]]\}
9.  \mforall{}[u:\{X.\mBbbI{},  0(\mBbbF{})  \mvdash{}  \_:A\}].  \mforall{}[a0:\{X  \mvdash{}  \_:(A)[0(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  u[0]]\}].  \mforall{}[cT:X.\mBbbI{}  \mvdash{}  Compositon(A)].
          ((fill  cT  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  u]  a0)[1(\mBbbI{})]  =  comp  cT  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  u]  a0)
10.  (fill  (cA)1(X.\mBbbI{})  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{}).1]  pr.1)[1(\mBbbI{})]  =  comp  (cA)1(X.\mBbbI{})  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{}).1]  pr.1
\mvdash{}  (fill  (cA)1(X.\mBbbI{})  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{}).1]  pr.1)[1(\mBbbI{})]  =  transprt(X;cA;pr.1)


By

---

Latex:
(Thin  (-2)
  THEN  NthHypEqGen  (-1)
  THEN  EqCDA
  THEN  Assert  \mkleeneopen{}transprt(X;(cA)1(X.\mBbbI{});pr.1)  =  comp  (cA)1(X.\mBbbI{})  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  discr(\mcdot{}).1]  pr.1\mkleeneclose{}\mcdot{})

---

Home Index