---

Step * of Lemma fill-type-down_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)].
  (fill-type-down(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:(((A)[1(𝕀)])p ⟶ A)})
BY
{ (Intros
   THEN ((InstLemma `csm-adjoin_wf` [⌜Gamma⌝;⌜Gamma.𝕀⌝;𝕀;⌜p⌝;⌜1-(q)⌝]⋅
          THENA (Auto THEN RWO "csm-interval-type" 0 THEN Auto)
          )
         THEN (Assert (cA)(p;1-(q)) ∈ Gamma.𝕀 ⊢ CompOp((A)-) BY
                     Auto)
         )
   THEN Unfold `fill-type-down` 0
   THEN (InstLemma `fill-type-up_wf` [⌜Gamma⌝;⌜(A)-⌝;⌜(cA)(p;1-(q))⌝]⋅ THENA Auto)
   THEN (InstLemma `cubical-fun_wf` [⌜Gamma.𝕀⌝;⌜(((A)-)[0(𝕀)])p⌝;⌜(A)-⌝]⋅ THENA Auto)
   THEN (InstLemma `csm-ap-term_wf` [⌜Gamma.𝕀⌝;⌜Gamma.𝕀⌝;⌜((((A)-)[0(𝕀)])p ⟶ (A)-)⌝;⌜(p;1-(q))⌝;
         ⌜fill-type-up(Gamma;(A)-;(cA)(p;1-(q)))⌝]⋅
         THENA Auto
         )
   THEN (InferEqualType THEN Try (Trivial))
   THEN EqCDA) }

1
.....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.𝕀)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  CompOp(A)].
    (fill-type-down(Gamma;A;cA)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:(((A)[1(\mBbbI{})])p  {}\mrightarrow{}  A)\})


By

---

Latex:
(Intros
  THEN  ((InstLemma  `csm-adjoin\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mBbbI{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}1-(q)\mkleeneclose{}]\mcdot{}
                THENA  (Auto  THEN  RWO  "csm-interval-type"  0  THEN  Auto)
                )
              THEN  (Assert  (cA)(p;1-(q))  \mmember{}  Gamma.\mBbbI{}  \mvdash{}  CompOp((A)-)  BY
                                      Auto)
              )
  THEN  Unfold  `fill-type-down`  0
  THEN  (InstLemma  `fill-type-up\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}(A)-\mkleeneclose{};\mkleeneopen{}(cA)(p;1-(q))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `cubical-fun\_wf`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}(((A)-)[0(\mBbbI{})])p\mkleeneclose{};\mkleeneopen{}(A)-\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((((A)-)[0(\mBbbI{})])p  {}\mrightarrow{}  (A)-)\mkleeneclose{};\mkleeneopen{}(p;1-(q))\mkleeneclose{};
              \mkleeneopen{}fill-type-up(Gamma;(A)-;(cA)(p;1-(q)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (InferEqualType  THEN  Try  (Trivial))
  THEN  EqCDA)

---

Home Index