---

Step * 1 1 of Lemma fill-type-up-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))[1(𝕀)] ∈ {Gamma ⊢ _:(A)[1(𝕀)]}
7. I : fset(ℕ)
8. a : Gamma(I)
⊢ ((app(fill-type-up(Gamma;A;cA); (u)p))[1(𝕀)] I a) = (app(transport-fun(Gamma;A;cA); u) I a) ∈ (A)[1(𝕀)](a)
BY
{ ((RepUR ``cubical-app csm-ap-term fill-type-up cubical-lambda`` 0
    THEN (Subst' (swap-interval(Gamma;(A)[0(𝕀)]))(1(([1(𝕀)])a);u I (p)([1(𝕀)])a) ~ <<1(a), u I a>, 1> 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-1-sq" 0
                 THEN Auto)
          )
    )
   THEN Fold `cubical-term-at` 0
   THEN (GenConclTerm ⌜u(a)⌝⋅ THENA 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))[1(𝕀)] ∈ {Gamma ⊢ _:(A)[1(𝕀)]}
7. I : fset(ℕ)
8. a : Gamma(I)
9. v : (A)[0(𝕀)](a)
10. u(a) = v ∈ (A)[0(𝕀)](a)
⊢ fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q(<<1(a), v>, 1>) = (transport-fun(Gamma;A;cA)(a)(1) v) ∈ (A)[1(𝕀)](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))[1(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}
7.  I  :  fset(\mBbbN{})
8.  a  :  Gamma(I)
\mvdash{}  ((app(fill-type-up(Gamma;A;cA);  (u)p))[1(\mBbbI{})]  I  a)  =  (app(transport-fun(Gamma;A;cA);  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(([1(\mBbbI{})])a);u  I  (p)([1(\mBbbI{})])a)  \msim{}  <ə(a),  u  I  a>,  1>  \000C0
                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-1-sq"  0
                              THEN  Auto)
                )
    )
  THEN  Fold  `cubical-term-at`  0
  THEN  (GenConclTerm  \mkleeneopen{}u(a)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index