---

Step * of Lemma cubical-fiber-id-fun

No Annotations
∀X:j⊢. ∀T:{X ⊢ _}.  ∀[u:{X ⊢ _:T}]. (X ⊢ Fiber(cubical-id-fun(X);u) = Σ T (Path_(T)p (u)p q) ∈ {X ⊢ _})
BY
{ (Auto THEN RepUR ``cubical-fiber`` 0 THEN RepeatFor 2 (EqCDA)) }

1
.....subterm..... T:t
4:n
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. u : {X ⊢ _:T}
⊢ app((cubical-id-fun(X))p; q) = q ∈ {X.T ⊢ _:(T)p}

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  \mforall{}T:\{X  \mvdash{}  \_\}.    \mforall{}[u:\{X  \mvdash{}  \_:T\}].  (X  \mvdash{}  Fiber(cubical-id-fun(X);u)  =  \mSigma{}  T  (Path\_(T)p  (u)p  q))


By

---

Latex:
(Auto  THEN  RepUR  ``cubical-fiber``  0  THEN  RepeatFor  2  (EqCDA))

---

Home Index