---

Step * 1 1 of Lemma fill-type-down-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))[0(𝕀)] = u ∈ {Gamma ⊢ _:((A)-)[0(𝕀)]})
7. u : {Gamma ⊢ _:(A)[1(𝕀)]}
8. app((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[0(𝕀)]; (u)1(Gamma)) = u ∈ {Gamma ⊢ _:((A)-)[0(𝕀)]}
9. {Gamma ⊢ _:(A)[1(𝕀)]} = {Gamma ⊢ _:((A)-)[0(𝕀)]} ∈ 𝕌{[i' | j']}
⊢ app(((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[1(𝕀)]; (u)1(Gamma)) = u ∈ {Gamma ⊢ _:(A)[1(𝕀)]}
BY
{ (Subst' ((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[1(𝕀)] ~ (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[0(𝕀)] 0
THENM Eq
) }

1
.....equality..... 
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))[0(𝕀)] = u ∈ {Gamma ⊢ _:((A)-)[0(𝕀)]})
7. u : {Gamma ⊢ _:(A)[1(𝕀)]}
8. app((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[0(𝕀)]; (u)1(Gamma)) = u ∈ {Gamma ⊢ _:((A)-)[0(𝕀)]}
9. {Gamma ⊢ _:(A)[1(𝕀)]} = {Gamma ⊢ _:((A)-)[0(𝕀)]} ∈ 𝕌{[i' | j']}
⊢ ((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[1(𝕀)] ~ (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[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))[0(\mBbbI{})]  =  u)
7.  u  :  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}
8.  app((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[0(\mBbbI{})];  (u)1(Gamma))  =  u
9.  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}  =  \{Gamma  \mvdash{}  \_:((A)-)[0(\mBbbI{})]\}
\mvdash{}  app(((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[1(\mBbbI{})];  (u)1(Gamma))  =  u


By

---

Latex:
(Subst'  ((fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)))[1(\mBbbI{})] 
  \msim{}  (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))[0(\mBbbI{})]  0
THENM  Eq
)

---

Home Index