---

Step * of Lemma fill-type-down-0

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)]. ∀[u:{Gamma ⊢ _:(A)[1(𝕀)]}].
  ((app(fill-type-down(Gamma;A;cA); (u)p))[0(𝕀)] = app(rev-transport-fun(Gamma;A;cA); u) ∈ {Gamma ⊢ _:(A)[0(𝕀)]})
BY
{ ((InstLemma `fill-type-up-1` [] THEN ParallelLast')
   THEN Intro
   THEN (InstHyp [⌜(A)-⌝] (-2)⋅ THENA Auto)
   THEN Thin (-3)
   THEN Intro
   THEN (InstLemmaIJ `csm-adjoin_wf` [⌜Gamma⌝;⌜Gamma.𝕀⌝;𝕀;⌜p⌝;⌜1-(q)⌝]⋅
         THENA (Auto THEN RWO "csm-interval-type" 0 THEN Auto)
         )
   THEN (Assert (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-) BY
               Auto)
   THEN (InstHyp [⌜(cA)(p;1-(q))⌝] (-4)⋅ THENA Auto)
   THEN Thin (-5)
   THEN ParallelLast
   THEN (Assert {Gamma ⊢ _:(A)[0(𝕀)]} = {Gamma ⊢ _:((A)-)[1(𝕀)]} ∈ 𝕌{[i' | j']} BY
               (EqCDA 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))); (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(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  CompOp(A)].  \mforall{}[u:\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}].
    ((app(fill-type-down(Gamma;A;cA);  (u)p))[0(\mBbbI{})]  =  app(rev-transport-fun(Gamma;A;cA);  u))


By

---

Latex:
((InstLemma  `fill-type-up-1`  []  THEN  ParallelLast')
  THEN  Intro
  THEN  (InstHyp  [\mkleeneopen{}(A)-\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  Thin  (-3)
  THEN  Intro
  THEN  (InstLemmaIJ  `csm-adjoin\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mBbbI{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}1-(q)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RWO  "csm-interval-type"  0  THEN  Auto)
              )
  THEN  (Assert  (cA)(p;1-(q))  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  CompOp((A)-)  BY
                          Auto)
  THEN  (InstHyp  [\mkleeneopen{}(cA)(p;1-(q))\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  Thin  (-5)
  THEN  ParallelLast
  THEN  (Assert  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}  =  \{Gamma  \mvdash{}  \_:((A)-)[1(\mBbbI{})]\}  BY
                          (EqCDA  THEN  Auto)))

---

Home Index