---

Step * 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. {X ⊢ _:(Path_Σ A B x y)}
⊢ {X ⊢ _:(Path_A x.1 y.1)}
BY
{ (RenameVar `p' (-1) THEN (InstLemma `path-eta_wf` [⌜X⌝;⌜Σ A B⌝;⌜p⌝]⋅ THENA Auto)) }

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}
⊢ {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.  \{X  \mvdash{}  \_:(Path\_\mSigma{}  A  B  x  y)\}
\mvdash{}  \{X  \mvdash{}  \_:(Path\_A  x.1  y.1)\}


By

---

Latex:
(RenameVar  `p'  (-1)  THEN  (InstLemma  `path-eta\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}\mSigma{}  A  B\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index