---

Step * of Lemma id-fiber-contraction_wf

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}].
  (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 (id-fiber-center(X;T))p q)})
BY
{ (Auto
   THEN (Assert id-fiber-center(X;T) ∈ {X.T ⊢ _:Σ (T)p (Path_((T)p)p (q)p q)} BY
               Auto)
   THEN Unfold `id-fiber-center` -1
   THEN Unfold `id-fiber-center` 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)}
⊢ 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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \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  (id-fiber-center(X;T))p  q)\})


By

---

Latex:
(Auto
  THEN  (Assert  id-fiber-center(X;T)  \mmember{}  \{X.T  \mvdash{}  \_:\mSigma{}  (T)p  (Path\_((T)p)p  (q)p  q)\}  BY
                          Auto)
  THEN  Unfold  `id-fiber-center`  -1
  THEN  Unfold  `id-fiber-center`  0)

---

Home Index