---

Step * 1 of Lemma fill-type-down-0


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. (p;1-(q)) ∈ cube_set_map{[i | [i | j]]:l}(Gamma.𝕀; Gamma.𝕀)
5. (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-)
6. ∀[u:{Gamma ⊢ _:((A)-)[0(𝕀)]}]
     ((app(fill-type-up(Gamma;(A)-;(cA)(p;1-(q))); (u)p))[1(𝕀)]
     = app(transport-fun(Gamma;(A)-;(cA)(p;1-(q))); u)
     ∈ {Gamma ⊢ _:((A)-)[1(𝕀)]})
7. u : {Gamma ⊢ _:(A)[1(𝕀)]}
8. (app(fill-type-up(Gamma;(A)-;(cA)(p;1-(q))); (u)p))[1(𝕀)]
= app(transport-fun(Gamma;(A)-;(cA)(p;1-(q))); u)
∈ {Gamma ⊢ _:((A)-)[1(𝕀)]}
9. {Gamma ⊢ _:(A)[0(𝕀)]} = {Gamma ⊢ _:((A)-)[1(𝕀)]} ∈ 𝕌{[i' | j']}
⊢ (app(fill-type-down(Gamma;A;cA); (u)p))[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); u) ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
BY
{ (((Unfold `fill-type-down` 0 THEN (RWO "csm-cubical-app" 0 THENA Auto)) THEN Reduce 0)
   THEN (RWO "csm-cubical-app" (-2) THENA Auto)
   THEN Reduce -2
   THEN (Subst' ((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[0(𝕀)] 
         ~ (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[1(𝕀)] 0
         THENA (CsmUnfolding THEN Auto THEN RepUR ``interval-rev cubical-term-at`` 0 THEN Auto)
         )) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. (p;1-(q)) ∈ cube_set_map{[i | [i | j]]:l}(Gamma.𝕀; Gamma.𝕀)
5. (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-)
6. ∀[u:{Gamma ⊢ _:((A)-)[0(𝕀)]}]
     ((app(fill-type-up(Gamma;(A)-;(cA)(p;1-(q))); (u)p))[1(𝕀)]
     = app(transport-fun(Gamma;(A)-;(cA)(p;1-(q))); u)
     ∈ {Gamma ⊢ _:((A)-)[1(𝕀)]})
7. u : {Gamma ⊢ _:(A)[1(𝕀)]}
8. app((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[1(𝕀)]; (u)1(Gamma))
= app(transport-fun(Gamma;(A)-;(cA)(p;1-(q))); u)
∈ {Gamma ⊢ _:((A)-)[1(𝕀)]}
9. {Gamma ⊢ _:(A)[0(𝕀)]} = {Gamma ⊢ _:((A)-)[1(𝕀)]} ∈ 𝕌{[i' | j']}
⊢ app((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[1(𝕀)]; (u)1(Gamma))
= app(rev-transport-fun(Gamma;A;cA); u)
∈ {Gamma ⊢ _:(A)[0(𝕀)]}

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  (p;1-(q))  \mmember{}  cube\_set\_map\{[i  |  [i  |  j]]:l\}(Gamma.\mBbbI{};  Gamma.\mBbbI{})
5.  (cA)(p;1-(q))  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  CompOp((A)-)
6.  \mforall{}[u:\{Gamma  \mvdash{}  \_:((A)-)[0(\mBbbI{})]\}]
          ((app(fill-type-up(Gamma;(A)-;(cA)(p;1-(q)));  (u)p))[1(\mBbbI{})]
          =  app(transport-fun(Gamma;(A)-;(cA)(p;1-(q)));  u))
7.  u  :  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}
8.  (app(fill-type-up(Gamma;(A)-;(cA)(p;1-(q)));  (u)p))[1(\mBbbI{})]
=  app(transport-fun(Gamma;(A)-;(cA)(p;1-(q)));  u)
9.  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}  =  \{Gamma  \mvdash{}  \_:((A)-)[1(\mBbbI{})]\}
\mvdash{}  (app(fill-type-down(Gamma;A;cA);  (u)p))[0(\mBbbI{})]  =  app(rev-transport-fun(Gamma;A;cA);  u)


By

---

Latex:
(((Unfold  `fill-type-down`  0  THEN  (RWO  "csm-cubical-app"  0  THENA  Auto))  THEN  Reduce  0)
  THEN  (RWO  "csm-cubical-app"  (-2)  THENA  Auto)
  THEN  Reduce  -2
  THEN  (Subst'  ((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[0(\mBbbI{})] 
              \msim{}  (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[1(\mBbbI{})]  0
              THENA  (CsmUnfolding  THEN  Auto  THEN  RepUR  ``interval-rev  cubical-term-at``  0  THEN  Auto)
              ))

---

Home Index