---

Step * of Lemma fill-path_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)]. ∀[x:{Gamma ⊢ _:(A)[1(𝕀)]}]. ∀[y:{Gamma ⊢ _:(A)[0(𝕀)]}].
∀[z:{Gamma.𝕀 ⊢ _:((A)[0(𝕀)])p}].
  (fill-path(Gamma;A;cA;x;y;z) ∈ {Gamma ⊢ _:(Path_(A)[1(𝕀)] x app(transport-fun(Gamma;A;cA); y))}) supposing 
     (((z)[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); x) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}) and 
     ((z)[1(𝕀)] = y ∈ {Gamma ⊢ _:(A)[0(𝕀)]}))
BY
{ (InstLemma `fillpath_wf` []
   THEN RepeatFor 5 (ParallelLast')
   THEN (Assert Gamma.𝕀 ⊢ ((A)[0(𝕀)])p BY
               Auto)
   THEN (Assert Gamma.𝕀 ⊢ ((A)[1(𝕀)])p BY
               Auto)
   THEN Intro
   THEN (Assert (z)[1(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]} BY
               (InferEqualType THEN Reduce 0 THEN Auto))
   THEN (Assert (z)[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]} BY
               (InferEqualType THEN Reduce 0 THEN Auto))
   THEN (D 0 THENW Auto)
   THEN (D 0 THENA (EqualityIsType1 THEN Auto))
   THEN (InstHyp [⌜z⌝] 6⋅ THENA Auto)
   THEN Unfold `fill-path` 0
   THEN Assert ⌜{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']}⌝⋅) }

1
.....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']}

2
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']}
⊢ <>(fillpath(Gamma;A;cA;x;y;z)) ∈ {Gamma ⊢ _:(Path_(A)[1(𝕀)] x app(transport-fun(Gamma;A;cA); y))}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  CompOp(A)].  \mforall{}[x:\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}].
\mforall{}[y:\{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}].  \mforall{}[z:\{Gamma.\mBbbI{}  \mvdash{}  \_:((A)[0(\mBbbI{})])p\}].
    (fill-path(Gamma;A;cA;x;y;z)
      \mmember{}  \{Gamma  \mvdash{}  \_:(Path\_(A)[1(\mBbbI{})]  x  app(transport-fun(Gamma;A;cA);  y))\})  supposing 
          (((z)[0(\mBbbI{})]  =  app(rev-transport-fun(Gamma;A;cA);  x))  and 
          ((z)[1(\mBbbI{})]  =  y))


By

---

Latex:
(InstLemma  `fillpath\_wf`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  (Assert  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p  BY
                          Auto)
  THEN  (Assert  Gamma.\mBbbI{}  \mvdash{}  ((A)[1(\mBbbI{})])p  BY
                          Auto)
  THEN  Intro
  THEN  (Assert  (z)[1(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}  BY
                          (InferEqualType  THEN  Reduce  0  THEN  Auto))
  THEN  (Assert  (z)[0(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}  BY
                          (InferEqualType  THEN  Reduce  0  THEN  Auto))
  THEN  (D  0  THENW  Auto)
  THEN  (D  0  THENA  (EqualityIsType1  THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}z\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  Unfold  `fill-path`  0
  THEN  Assert  \mkleeneopen{}\{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']\}\mkleeneclose{}\mcdot{})

---

Home Index