---

Step * 1 of Lemma contr-witness_wf


1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. c : {X ⊢ _:A}
4. p : {X.A ⊢ _:(Path_(A)p (c)p q)}
⊢ (λp) ∈ {X ⊢ _:(Π(A)p (Path_((A)p)p (q)p q))[c]}
BY
{ (InferEqualTypeUp THENL [EqCDA; Auto]) }

1
.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. c : {X ⊢ _:A}
4. p : {X.A ⊢ _:(Path_(A)p (c)p q)}
⊢ X ⊢ ΠA (Path_(A)p (c)p q) = (Π(A)p (Path_((A)p)p (q)p q))[c] ∈ cubical-type{[j' | i']:l}(X)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}  \_\}
3.  c  :  \{X  \mvdash{}  \_:A\}
4.  p  :  \{X.A  \mvdash{}  \_:(Path\_(A)p  (c)p  q)\}
\mvdash{}  (\mlambda{}p)  \mmember{}  \{X  \mvdash{}  \_:(\mPi{}(A)p  (Path\_((A)p)p  (q)p  q))[c]\}


By

---

Latex:
(InferEqualTypeUp  THENL  [EqCDA;  Auto])

---

Home Index