---

Step * of Lemma csm-id-fiber-center

No Annotations
∀[G,K:j⊢]. ∀[tau:K j⟶ G]. ∀[A:{G ⊢ _}].
  (id-fiber-center(K;(A)tau) = (id-fiber-center(G;A))tau+ ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)})
BY
{ (Auto THEN Unfold `id-fiber-center` 0 THEN (RWO "csm-cubical-pair" 0 THENA Auto)) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ G
4. A : {G ⊢ _}
⊢ cubical-pair(q;refl(q)) = cubical-pair((q)tau+;(refl(q))tau+) ∈ {K.(A)tau ⊢ _:Fiber((cubical-id-fun(K))p;q)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  G].  \mforall{}[A:\{G  \mvdash{}  \_\}].    (id-fiber-center(K;(A)tau)  =  (id-fiber-center(G;A))tau+)


By

---

Latex:
(Auto  THEN  Unfold  `id-fiber-center`  0  THEN  (RWO  "csm-cubical-pair"  0  THENA  Auto))

---

Home Index