---

Step * 1 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))))[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(𝕀)]}
BY
{ (Fold `rev-transport-fun` (-2) THEN Eq) }

---

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))))[1(\mBbbI{})];  (u)1(Gamma))
=  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-up(Gamma;(A)-;(cA)(p;1-(q))))[1(\mBbbI{})];  (u)1(Gamma))
=  app(rev-transport-fun(Gamma;A;cA);  u)


By

---

Latex:
(Fold  `rev-transport-fun`  (-2)  THEN  Eq)

---

Home Index