---

Step * of Lemma pcw-path-shift

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P].
  ∀path:Path. (λx.(path (x + 1)) ∈ Path)
BY
{ (Auto THEN D -1 THEN (MemTypeCD THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
    \mforall{}path:Path.  (\mlambda{}x.(path  (x  +  1))  \mmember{}  Path)


By

---

Latex:
(Auto  THEN  D  -1  THEN  (MemTypeCD  THEN  Reduce  0)  THEN  Auto)

---

Home Index