---

Step * 1 of Lemma id-fiber-contraction_wf


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. cubical-pair(q;refl(q)) ∈ {X.T ⊢ _:Σ (T)p (Path_((T)p)p (q)p q)}
⊢ id-fiber-contraction(X;T) ∈ {X.T.Σ (T)p (Path_((T)p)p (q)p q) ⊢ _
                               :(Path_(Σ (T)p (Path_((T)p)p (q)p q))p (cubical-pair(q;refl(q)))p q)}
BY
{ Unfold `id-fiber-contraction` 0 }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. cubical-pair(q;refl(q)) ∈ {X.T ⊢ _:Σ (T)p (Path_((T)p)p (q)p q)}
⊢ (singleton-contraction(X.T.(T)p.(Path_((T)p)p (q)p q);q))SigmaElim
  ∈ {X.T.Σ (T)p (Path_((T)p)p (q)p q) ⊢ _:(Path_(Σ (T)p (Path_((T)p)p (q)p q))p (cubical-pair(q;refl(q)))p q)}

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  cubical-pair(q;refl(q))  \mmember{}  \{X.T  \mvdash{}  \_:\mSigma{}  (T)p  (Path\_((T)p)p  (q)p  q)\}
\mvdash{}  id-fiber-contraction(X;T)  \mmember{}  \{X.T.\mSigma{}  (T)p  (Path\_((T)p)p  (q)p  q)  \mvdash{}  \_:(Path\_(\mSigma{}  (T)p  (Path\_((T)p)p  (q)p
                                                                                                                                                                                q))p
                                                                                                                                                    (cubical-pair(q;refl(q)))p
                                                                                                                                                    q)\}


By

---

Latex:
Unfold  `id-fiber-contraction`  0

---

Home Index