---

Step * 1 of Lemma fill-path_wf

.....assertion..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[z:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}]
     (fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                    ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                    ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} ) supposi\000Cng 
        (((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and 
        ((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                  ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                  ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} 
⊢ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
   ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} 
  ∈ 𝕌{[i | j']}
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[z:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}]
     (fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                    ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                    ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} ) supposi\000Cng 
        (((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and 
        ((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                  ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                  ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} 
⊢ {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p} ∈ 𝕌{[i | j']}

2
.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. x : {Gamma ⊢ _:(A)[1(𝕀)]}
5. y : {Gamma ⊢ _:(A)[0(𝕀)]}
6. ∀[z:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}]
     (fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                    ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                    ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} ) supposi\000Cng 
        (((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and 
        ((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
7. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
8. Gamma.𝕀 ⊢ ((A)[1(𝕀)])p
9. z : {Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}
10. (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
11. (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
12. (z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
13. (z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
14. fillpath(Gamma;A;cA;x;y;z) ∈ {t:{Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}| 
                                  ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
                                  ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})} 
15. t : {Gamma.𝕀 ⊢ _:((A)[1(𝕀)])p}
⊢ ((t)[0(𝕀)] = x ∈ {Gamma ⊢ _:(A)[1(𝕀)]}) ∧ ((t)[1(𝕀)] = app(transport-fun(Gamma;A;cA); y) ∈ {Gamma ⊢ _:(A)[1(𝕀)]})
  ∈ 𝕌{[i | j']}

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  x  :  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}
5.  y  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
6.  \mforall{}[z:\{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[0(\mBbbI{})])p\}]
          (fillpath(Gamma;A;cA;x;y;z)  \mmember{}  \{t:\{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[1(\mBbbI{})])p\}| 
                                                                        ((t)[0(\mBbbI{})]  =  x)
                                                                        \mwedge{}  ((t)[1(\mBbbI{})]  =  app(transport-fun(Gamma;A;cA);  y))\}  )  supposing 
                (((z)[0(\mBbbI{})]  =  app(rev-transport-fun(Gamma;A;cA);  x))  and 
                ((z)[1(\mBbbI{})]  =  y))
7.  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p
8.  Gamma.\mBbbI{}  \mvdash{}  ((A)[1(\mBbbI{})])p
9.  z  :  \{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[0(\mBbbI{})])p\}
10.  (z)[1(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
11.  (z)[0(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
12.  (z)[1(\mBbbI{})]  =  y
13.  (z)[0(\mBbbI{})]  =  app(rev-transport-fun(Gamma;A;cA);  x)
14.  fillpath(Gamma;A;cA;x;y;z)  \mmember{}  \{t:\{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[1(\mBbbI{})])p\}| 
                                                                    ((t)[0(\mBbbI{})]  =  x)
                                                                    \mwedge{}  ((t)[1(\mBbbI{})]  =  app(transport-fun(Gamma;A;cA);  y))\} 
\mvdash{}  \{t:\{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[1(\mBbbI{})])p\}|  ((t)[0(\mBbbI{})]  =  x)  \mwedge{}  ((t)[1(\mBbbI{})]  =  app(transport-fun(Gamma;A;cA);  y))\} 
    \mmember{}  \mBbbU{}\{[i  |  j']\}


By

---

Latex:
MemCD

---

Home Index