---

Step * 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(𝕀)]}
⊢ (app(fill-type-up(Gamma;A;cA); (u)p))[1(𝕀)] = app(transport-fun(Gamma;A;cA); u) ∈ {Gamma ⊢ _:(A)[1(𝕀)]}
BY
{ ((Assert (app(fill-type-up(Gamma;A;cA); (u)p))[1(𝕀)] ∈ {Gamma ⊢ _:(A)[1(𝕀)]} BY
          ((GenConclTerm ⌜fill-type-up(Gamma;A;cA)⌝⋅ THENA Auto)
           THEN GenConcl ⌜app(v; (u)p) = w ∈ {Gamma.𝕀 ⊢ _:A}⌝⋅
           THEN Auto))
   THEN (CubicalTermEqual 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)
⊢ ((app(fill-type-up(Gamma;A;cA); (u)p))[1(𝕀)] I a) = (app(transport-fun(Gamma;A;cA); u) I a) ∈ (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{})]\}
\mvdash{}  (app(fill-type-up(Gamma;A;cA);  (u)p))[1(\mBbbI{})]  =  app(transport-fun(Gamma;A;cA);  u)


By

---

Latex:
((Assert  (app(fill-type-up(Gamma;A;cA);  (u)p))[1(\mBbbI{})]  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}  BY
                ((GenConclTerm  \mkleeneopen{}fill-type-up(Gamma;A;cA)\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  GenConcl  \mkleeneopen{}app(v;  (u)p)  =  w\mkleeneclose{}\mcdot{}
                  THEN  Auto))
  THEN  (CubicalTermEqual  THENA  Auto)
  )

---

Home Index