---

Step * 1 of Lemma fill-type-down_wf

.....subterm..... T:t
2:n
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. (p;1-(q)) ∈ Gamma.𝕀 ij⟶ Gamma.𝕀
5. (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-)
6. fill-type-up(Gamma;(A)-;(cA)(p;1-(q))) ∈ {Gamma.𝕀 ⊢ _:((((A)-)[0(𝕀)])p ⟶ (A)-)}
7. Gamma.𝕀 ⊢ ((((A)-)[0(𝕀)])p ⟶ (A)-)
8. (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)) ∈ {Gamma.𝕀 ⊢ _:(((((A)-)[0(𝕀)])p ⟶ (A)-))(p;1-(q))}
⊢ (((((A)-)[0(𝕀)])p ⟶ (A)-))(p;1-(q)) = (Gamma.𝕀 ⊢ ((A)[1(𝕀)])p ⟶ A) ∈ cubical-type{[j' | i']:l}(Gamma.𝕀)
BY
{ (InstLemma `csm-cubical-fun` [⌜Gamma.𝕀⌝;⌜Gamma.𝕀⌝;⌜(((A)-)[0(𝕀)])p⌝;⌜(A)-⌝;⌜(p;1-(q))⌝]⋅ THENA Auto) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. (p;1-(q)) ∈ Gamma.𝕀 ij⟶ Gamma.𝕀
5. (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-)
6. fill-type-up(Gamma;(A)-;(cA)(p;1-(q))) ∈ {Gamma.𝕀 ⊢ _:((((A)-)[0(𝕀)])p ⟶ (A)-)}
7. Gamma.𝕀 ⊢ ((((A)-)[0(𝕀)])p ⟶ (A)-)
8. (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q)) ∈ {Gamma.𝕀 ⊢ _:(((((A)-)[0(𝕀)])p ⟶ (A)-))(p;1-(q))}
9. (((((A)-)[0(𝕀)])p ⟶ (A)-))(p;1-(q)) = (Gamma.𝕀 ⊢ ((((A)-)[0(𝕀)])p)(p;1-(q)) ⟶ ((A)-)(p;1-(q))) ∈ {Gamma.𝕀 ⊢ _}
⊢ (((((A)-)[0(𝕀)])p ⟶ (A)-))(p;1-(q)) = (Gamma.𝕀 ⊢ ((A)[1(𝕀)])p ⟶ A) ∈ cubical-type{[j' | i']:l}(Gamma.𝕀)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  cA  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  (p;1-(q))  \mmember{}  Gamma.\mBbbI{}  ij{}\mrightarrow{}  Gamma.\mBbbI{}
5.  (cA)(p;1-(q))  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  CompOp((A)-)
6.  fill-type-up(Gamma;(A)-;(cA)(p;1-(q)))  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:((((A)-)[0(\mBbbI{})])p  {}\mrightarrow{}  (A)-)\}
7.  Gamma.\mBbbI{}  \mvdash{}  ((((A)-)[0(\mBbbI{})])p  {}\mrightarrow{}  (A)-)
8.  (fill-type-up(Gamma;(A)-;(cA)(p;1-(q))))(p;1-(q))
      \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:(((((A)-)[0(\mBbbI{})])p  {}\mrightarrow{}  (A)-))(p;1-(q))\}
\mvdash{}  (((((A)-)[0(\mBbbI{})])p  {}\mrightarrow{}  (A)-))(p;1-(q))  =  (Gamma.\mBbbI{}  \mvdash{}  ((A)[1(\mBbbI{})])p  {}\mrightarrow{}  A)


By

---

Latex:
(InstLemma  `csm-cubical-fun`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(((A)-)[0(\mBbbI{})])p\mkleeneclose{};\mkleeneopen{}(A)-\mkleeneclose{};\mkleeneopen{}(p;1-(q))\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index