---

Step * 1 1 of Lemma coW-equiv_weakening


1. [A] : 𝕌'
2. B : A ⟶ Type@i'
3. w : coW(A;a.B[a])@i'
4. w' : coW(A;a.B[a])@i'
5. w = w' ∈ coW(A;a.B[a])
6. () = () ∈ copath(a.B a;w')
7. p1 : copath(a.B a;w')@i
8. p2 : copath(a.B a;w')@i
9. [%6] : p1 = p2 ∈ copath(a.B a;w')@i
10. q1 : copath(a.B a;w')@i
11. q2 : copath(a.B a;w')@i
12. [%4] : ((copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ)
∧ copathAgree(a.B a;w';p1;q1)
∧ (p2 = q2 ∈ copath(a.B a;w')))
∨ ((p1 = q1 ∈ copath(a.B a;w')) ∧ (copath-length(q2) = (copath-length(p2) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';p2;q2))@i
13. let u,v = if copath-length(p1) <z copath-length(q1) then <q1, q1> else <q2, q2> fi  
    in u = v ∈ copath(a.B a;w')
14. copath-length(p1) < copath-length(q1)
⊢ ((copath-length(q1) = (copath-length(q1) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';q1;q1) ∧ (q2 = q1 ∈ copath(a.B a;w')))
∨ ((q1 = q1 ∈ copath(a.B a;w')) ∧ (copath-length(q1) = (copath-length(q2) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';q2;q1))
BY
{ ((OrRight THEN Auto) THEN SplitOrHyps THEN Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type@i'
3. w : coW(A;a.B[a])@i'
4. w' : coW(A;a.B[a])@i'
5. w = w' ∈ coW(A;a.B[a])
6. () = () ∈ copath(a.B a;w')
7. p1 : copath(a.B a;w')@i
8. p2 : copath(a.B a;w')@i
9. p1 = p2 ∈ copath(a.B a;w')
10. q1 : copath(a.B a;w')@i
11. q2 : copath(a.B a;w')@i
12. p1 = q1 ∈ copath(a.B a;w')
13. copath-length(q2) = (copath-length(p2) + 1) ∈ ℤ
14. copathAgree(a.B a;w';p2;q2)
15. let u,v = if copath-length(p1) <z copath-length(q1) then <q1, q1> else <q2, q2> fi  
    in u = v ∈ copath(a.B a;w')
16. copath-length(p1) < copath-length(q1)
17. q1 = q1 ∈ copath(a.B a;w')
⊢ copath-length(q1) = (copath-length(q2) + 1) ∈ ℤ

2
1. [A] : 𝕌'
2. B : A ⟶ Type@i'
3. w : coW(A;a.B[a])@i'
4. w' : coW(A;a.B[a])@i'
5. w = w' ∈ coW(A;a.B[a])
6. () = () ∈ copath(a.B a;w')
7. p1 : copath(a.B a;w')@i
8. p2 : copath(a.B a;w')@i
9. [%6] : p1 = p2 ∈ copath(a.B a;w')@i
10. q1 : copath(a.B a;w')@i
11. q2 : copath(a.B a;w')@i
12. [%4] : ((copath-length(q1) = (copath-length(p1) + 1) ∈ ℤ)
∧ copathAgree(a.B a;w';p1;q1)
∧ (p2 = q2 ∈ copath(a.B a;w')))
∨ ((p1 = q1 ∈ copath(a.B a;w')) ∧ (copath-length(q2) = (copath-length(p2) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';p2;q2))@i
13. let u,v = if copath-length(p1) <z copath-length(q1) then <q1, q1> else <q2, q2> fi  
    in u = v ∈ copath(a.B a;w')
14. copath-length(p1) < copath-length(q1)
15. q1 = q1 ∈ copath(a.B a;w')
16. copath-length(q1) = (copath-length(q2) + 1) ∈ ℤ
⊢ copathAgree(a.B a;w';q2;q1)

---

Latex:

---

Latex:

1.  [A]  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type@i'
3.  w  :  coW(A;a.B[a])@i'
4.  w'  :  coW(A;a.B[a])@i'
5.  w  =  w'
6.  ()  =  ()
7.  p1  :  copath(a.B  a;w')@i
8.  p2  :  copath(a.B  a;w')@i
9.  [\%6]  :  p1  =  p2@i
10.  q1  :  copath(a.B  a;w')@i
11.  q2  :  copath(a.B  a;w')@i
12.  [\%4]  :  ((copath-length(q1)  =  (copath-length(p1)  +  1))  \mwedge{}  copathAgree(a.B  a;w';p1;q1)  \mwedge{}  (p2  =  q2))
\mvee{}  ((p1  =  q1)  \mwedge{}  (copath-length(q2)  =  (copath-length(p2)  +  1))  \mwedge{}  copathAgree(a.B  a;w';p2;q2))@i
13.  let  u,v  =  if  copath-length(p1)  <z  copath-length(q1)  then  <q1,  q1>  else  <q2,  q2>  fi   
        in  u  =  v
14.  copath-length(p1)  <  copath-length(q1)
\mvdash{}  ((copath-length(q1)  =  (copath-length(q1)  +  1))  \mwedge{}  copathAgree(a.B  a;w';q1;q1)  \mwedge{}  (q2  =  q1))
\mvee{}  ((q1  =  q1)  \mwedge{}  (copath-length(q1)  =  (copath-length(q2)  +  1))  \mwedge{}  copathAgree(a.B  a;w';q2;q1))


By

---

Latex:
((OrRight  THEN  Auto)  THEN  SplitOrHyps  THEN  Auto)

---

Home Index