---

Step * 1 1 of Lemma sigma-path-fst


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. x : {X ⊢ _:Σ A B}
5. y : {X ⊢ _:Σ A B}
6. p : {X ⊢ _:(Path_Σ A B x y)}
7. path-eta(p) ∈ {X.𝕀 ⊢ _:(Σ A B)p}
⊢ {X ⊢ _:(Path_A x.1 y.1)}
BY
{ UseWitness ⌜<>(path-eta(p).1)⌝⋅ }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. x : {X ⊢ _:Σ A B}
5. y : {X ⊢ _:Σ A B}
6. p : {X ⊢ _:(Path_Σ A B x y)}
7. path-eta(p) ∈ {X.𝕀 ⊢ _:(Σ A B)p}
⊢ <>(path-eta(p).1) ∈ {X ⊢ _:(Path_A x.1 y.1)}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  x  :  \{X  \mvdash{}  \_:\mSigma{}  A  B\}
5.  y  :  \{X  \mvdash{}  \_:\mSigma{}  A  B\}
6.  p  :  \{X  \mvdash{}  \_:(Path\_\mSigma{}  A  B  x  y)\}
7.  path-eta(p)  \mmember{}  \{X.\mBbbI{}  \mvdash{}  \_:(\mSigma{}  A  B)p\}
\mvdash{}  \{X  \mvdash{}  \_:(Path\_A  x.1  y.1)\}


By

---

Latex:
UseWitness  \mkleeneopen{}<>(path-eta(p).1)\mkleeneclose{}\mcdot{}

---

Home Index