---

Step * 1 1 2 1 1 1 1 of Lemma pcw-path-copathAgree


1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. w : coW(A;a.B[a])@i'
4. n : ℕ@i
5. v1 : coPath(a.B[a];w;n)@i
6. xx : Top@i
⊢ ↓coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx))
BY
{ Assert ⌜(coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)) ∈ Type)
          ∧ (↓coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)))⌝⋅ }

1
.....assertion..... 
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. w : coW(A;a.B[a])@i'
4. n : ℕ@i
5. v1 : coPath(a.B[a];w;n)@i
6. xx : Top@i
⊢ (coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)) ∈ Type) ∧ (↓coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)))

2
1. [A] : 𝕌'
2. [B] : A ⟶ Type
3. w : coW(A;a.B[a])@i'
4. n : ℕ@i
5. v1 : coPath(a.B[a];w;n)@i
6. xx : Top@i
7. (coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)) ∈ Type) ∧ (↓coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)))
⊢ ↓coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx))

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])@i'
4.  n  :  \mBbbN{}@i
5.  v1  :  coPath(a.B[a];w;n)@i
6.  xx  :  Top@i
\mvdash{}  \mdownarrow{}coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx))


By

---

Latex:
Assert  \mkleeneopen{}(coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx))  \mmember{}  Type)
                \mwedge{}  (\mdownarrow{}coPathAgree(a.B[a];n;w;v1;coPath-extend(n;v1;xx)))\mkleeneclose{}\mcdot{}

---

Home Index