---

Step * 1 of Lemma id-fiber-center_wf


1. X : CubicalSet{j}
2. T : {X ⊢ _}
⊢ refl(q) ∈ {X.T ⊢ _:((Path_((T)p)p (q)p q))[q]}
BY
{ ((Assert refl(q) ∈ {X.T ⊢ _:(Path_(T)p q q)} BY
          Auto)
   THEN InferEqualTypeUp
   THEN EqCDA
   THEN (Assert [q] ∈ X.T ij⟶ X.T.(T)p BY
               Auto)⋅
   THEN (RWO  "csm-path-type" 0 THENA Auto)
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
\mvdash{}  refl(q)  \mmember{}  \{X.T  \mvdash{}  \_:((Path\_((T)p)p  (q)p  q))[q]\}


By

---

Latex:
((Assert  refl(q)  \mmember{}  \{X.T  \mvdash{}  \_:(Path\_(T)p  q  q)\}  BY
                Auto)
  THEN  InferEqualTypeUp
  THEN  EqCDA
  THEN  (Assert  [q]  \mmember{}  X.T  ij{}\mrightarrow{}  X.T.(T)p  BY
                          Auto)\mcdot{}
  THEN  (RWO    "csm-path-type"  0  THENA  Auto)
  THEN  EqCDA
  THEN  Auto)

---

Home Index