Step * 1 1 of Lemma fst-transprt-sigma


1. CubicalSet{j}
2. {X.𝕀 ⊢ _}
3. {X.𝕀.A ⊢ _}
4. cA X.𝕀 +⊢ Compositon(A)
5. cB X.𝕀.A +⊢ Compositon(B)
6. pr {X ⊢ _:(Σ B)[0(𝕀)]}
7. (cA)1(X.𝕀) ∈ X.𝕀 +⊢ Compositon(A)
⊢ pr.1 ∈ {X ⊢ _:(A)[0(𝕀)]}
BY
(InstLemmaIJ `csm-cubical-sigma` [⌜X.𝕀⌝;⌜X⌝;⌜A⌝;⌜B⌝;⌜[0(𝕀)]⌝]⋅ THENA Auto) }

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


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)
\mvdash{}  pr.1  \mmember{}  \{X  \mvdash{}  \_:(A)[0(\mBbbI{})]\}


By


Latex:
(InstLemmaIJ  `csm-cubical-sigma`  [\mkleeneopen{}X.\mBbbI{}\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}[0(\mBbbI{})]\mkleeneclose{}]\mcdot{}  THENA  Auto)




Home Index