---

Step * 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])
⊢ ∃F:p:{p:copath(a.B a;w') × copath(a.B a;w')| let u,v = p in u = v ∈ copath(a.B a;w')} 
     ⟶ q:{q:copath(a.B a;w') × copath(a.B a;w')| 
           let u,v = p 
           in let u',v' = q 
              in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                 ∧ copathAgree(a.B a;w';u;u')
                 ∧ (v = v' ∈ copath(a.B a;w')))
                 ∨ ((u = u' ∈ copath(a.B a;w'))
                   ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                   ∧ copathAgree(a.B a;w';v;v'))} 
     ⟶ (copath(a.B a;w') × copath(a.B a;w'))
   ((() = () ∈ copath(a.B a;w'))
   ∧ (∀p:{p:copath(a.B a;w') × copath(a.B a;w')| let u,v = p in u = v ∈ copath(a.B a;w')} .
      ∀q:{q:copath(a.B a;w') × copath(a.B a;w')| 
          let u,v = p 
          in let u',v' = q 
             in ((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B a;w';u;u')
                ∧ (v = v' ∈ copath(a.B a;w')))
                ∨ ((u = u' ∈ copath(a.B a;w'))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B a;w';v;v'))} .
        (let u,v = F p q 
         in u = v ∈ copath(a.B a;w')
        ∧ let u,v = q 
          in let u',v' = F p q 
             in (((copath-length(u') = (copath-length(u) + 1) ∈ ℤ)
                ∧ copathAgree(a.B a;w';u;u')
                ∧ (v = v' ∈ copath(a.B a;w')))
                ∨ ((u = u' ∈ copath(a.B a;w'))
                  ∧ (copath-length(v') = (copath-length(v) + 1) ∈ ℤ)
                  ∧ copathAgree(a.B a;w';v;v')))
                ∧ (copath-length(u') = copath-length(v') ∈ ℤ))))
BY
{ (D 0 With ⌜λp,q. let u,v = p 
                   in let u',v' = q 
                      in if copath-length(u) <z copath-length(u') then <u', u'> else <v', v'> fi ⌝ 
   THEN Auto
   THEN (DSetVars THEN DProds THEN All Reduce)
   THEN AutoSplit
   THEN D 0
   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. [%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))

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. ¬copath-length(p1) < copath-length(q1)
12. q2 : copath(a.B a;w')@i
13. [%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
14. q2 = q2 ∈ copath(a.B a;w')
⊢ ((copath-length(q2) = (copath-length(q1) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';q1;q2) ∧ (q2 = q2 ∈ copath(a.B a;w')))
∨ ((q1 = q2 ∈ copath(a.B a;w')) ∧ (copath-length(q2) = (copath-length(q2) + 1) ∈ ℤ) ∧ copathAgree(a.B a;w';q2;q2))

---

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'
\mvdash{}  \mexists{}F:p:\{p:copath(a.B  a;w')  \mtimes{}  copath(a.B  a;w')|  let  u,v  =  p  in  u  =  v\} 
          {}\mrightarrow{}  q:\{q:copath(a.B  a;w')  \mtimes{}  copath(a.B  a;w')| 
                      let  u,v  =  p 
                      in  let  u',v'  =  q 
                            in  ((copath-length(u')  =  (copath-length(u)  +  1))
                                  \mwedge{}  copathAgree(a.B  a;w';u;u')
                                  \mwedge{}  (v  =  v'))
                                  \mvee{}  ((u  =  u')
                                      \mwedge{}  (copath-length(v')  =  (copath-length(v)  +  1))
                                      \mwedge{}  copathAgree(a.B  a;w';v;v'))\} 
          {}\mrightarrow{}  (copath(a.B  a;w')  \mtimes{}  copath(a.B  a;w'))
      ((()  =  ())
      \mwedge{}  (\mforall{}p:\{p:copath(a.B  a;w')  \mtimes{}  copath(a.B  a;w')|  let  u,v  =  p  in  u  =  v\}  .
            \mforall{}q:\{q:copath(a.B  a;w')  \mtimes{}  copath(a.B  a;w')| 
                    let  u,v  =  p 
                    in  let  u',v'  =  q 
                          in  ((copath-length(u')  =  (copath-length(u)  +  1))
                                \mwedge{}  copathAgree(a.B  a;w';u;u')
                                \mwedge{}  (v  =  v'))
                                \mvee{}  ((u  =  u')
                                    \mwedge{}  (copath-length(v')  =  (copath-length(v)  +  1))
                                    \mwedge{}  copathAgree(a.B  a;w';v;v'))\}  .
                (let  u,v  =  F  p  q 
                  in  u  =  v
                \mwedge{}  let  u,v  =  q 
                    in  let  u',v'  =  F  p  q 
                          in  (((copath-length(u')  =  (copath-length(u)  +  1))
                                \mwedge{}  copathAgree(a.B  a;w';u;u')
                                \mwedge{}  (v  =  v'))
                                \mvee{}  ((u  =  u')
                                    \mwedge{}  (copath-length(v')  =  (copath-length(v)  +  1))
                                    \mwedge{}  copathAgree(a.B  a;w';v;v')))
                                \mwedge{}  (copath-length(u')  =  copath-length(v')))))


By

---

Latex:
(D  0  With  \mkleeneopen{}\mlambda{}p,q.  let  u,v  =  p 
                                  in  let  u',v'  =  q 
                                        in  if  copath-length(u)  <z  copath-length(u')  then  <u',  u'>  else  <v',  v'>  fi  \mkleeneclose{} 
  THEN  Auto
  THEN  (DSetVars  THEN  DProds  THEN  All  Reduce)
  THEN  AutoSplit
  THEN  D  0
  THEN  Auto)

---

Home Index