---

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


1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. u : {Gamma ⊢ _:(A)[0(𝕀)]}
6. (app(fill-type-up(Gamma;A;cA); (u)p))[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
7. I : fset(ℕ)
8. a : Gamma(I)
⊢ ((app(fill-type-up(Gamma;A;cA); (u)p))[0(𝕀)] I a) = (u I a) ∈ (A)[0(𝕀)](a)
BY
{ (RepUR ``cubical-app csm-ap-term fill-type-up cubical-lambda`` 0
   THEN (Subst' (swap-interval(Gamma;(A)[0(𝕀)]))(1(([0(𝕀)])a);u I (p)([0(𝕀)])a) ~ <<1(a), u I a>, 0> 0
         THENA (RepUR ``swap-interval csm-swap`` 0
                THEN CsmUnfoldingNotInterval
                THEN RepUR ``cube-context-adjoin`` 0
                THEN (RWO "interval-type-ap-morph" 0 THENA Auto)
                THEN RWO  "dM-lift-0-sq" 0
                THEN Auto)
         )
   ) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. u : {Gamma ⊢ _:(A)[0(𝕀)]}
6. (app(fill-type-up(Gamma;A;cA); (u)p))[0(𝕀)] ∈ {Gamma ⊢ _:(A)[0(𝕀)]}
7. I : fset(ℕ)
8. a : Gamma(I)
⊢ (fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q I <<1(a), u I a>, 0>) = (u I a) ∈ (A)[0(𝕀)](a)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p
5.  u  :  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
6.  (app(fill-type-up(Gamma;A;cA);  (u)p))[0(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[0(\mBbbI{})]\}
7.  I  :  fset(\mBbbN{})
8.  a  :  Gamma(I)
\mvdash{}  ((app(fill-type-up(Gamma;A;cA);  (u)p))[0(\mBbbI{})]  I  a)  =  (u  I  a)


By

---

Latex:
(RepUR  ``cubical-app  csm-ap-term  fill-type-up  cubical-lambda``  0
  THEN  (Subst'  (swap-interval(Gamma;(A)[0(\mBbbI{})]))(1(([0(\mBbbI{})])a);u  I  (p)([0(\mBbbI{})])a)  \msim{}  <ə(a),  u  I  a>,  0>  0
              THENA  (RepUR  ``swap-interval  csm-swap``  0
                            THEN  CsmUnfoldingNotInterval
                            THEN  RepUR  ``cube-context-adjoin``  0
                            THEN  (RWO  "interval-type-ap-morph"  0  THENA  Auto)
                            THEN  RWO    "dM-lift-0-sq"  0
                            THEN  Auto)
              )
  )

---

Home Index