---

Step * 1 of Lemma copath-eta


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. p : copath(a.B[a];w)
5. 0 < copath-length(p)
⊢ copath-cons(copath-hd(p);copath-tl(p)) = p ∈ copath(a.B[a];w)
BY
{ (RWO "copath-cons-hd-tl" 0 THEN Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. n : ℕ
5. p1 : coPath(a.B[a];w;n)
6. 0 < copath-length(<n, p1>)
⊢ p1 ∈ Top × Top

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  p  :  copath(a.B[a];w)
5.  0  <  copath-length(p)
\mvdash{}  copath-cons(copath-hd(p);copath-tl(p))  =  p


By

---

Latex:
(RWO  "copath-cons-hd-tl"  0  THEN  Auto)

---

Home Index