---

Step * 1 of Lemma fill-type-up_wf

.....assertion..... 
1. [Gamma] : CubicalSet{j}
2. [A] : {Gamma.𝕀 ⊢ _}
3. [cA] : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
⊢ fill-type-up(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p}
BY
{ ((Unfold `fill-type-up` 0 THEN (InstLemma `cubical-lambda_wf` [⌜Gamma.𝕀⌝;⌜((A)[0(𝕀)])p⌝;⌜(A)p⌝]⋅ THENA Auto))
   THEN BHyp -1
   ) }

1
.....wf..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. ∀[b:{Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}]. ((λb) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p})
⊢ (fill (cA)p+ [0(𝔽) ⊢→ discr(⋅)] q)swap-interval(Gamma;(A)[0(𝕀)]) ∈ {Gamma.𝕀.((A)[0(𝕀)])p ⊢ _:(A)p}

---

Latex:

---

Latex:
.....assertion..... 
1.  [Gamma]  :  CubicalSet\{j\}
2.  [A]  :  \{Gamma.\mBbbI{}  \mvdash{}  \_\}
3.  [cA]  :  Gamma.\mBbbI{}  \mvdash{}  CompOp(A)
4.  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p
\mvdash{}  fill-type-up(Gamma;A;cA)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:\mPi{}((A)[0(\mBbbI{})])p  (A)p\}


By

---

Latex:
((Unfold  `fill-type-up`  0
    THEN  (InstLemma  `cubical-lambda\_wf`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((A)[0(\mBbbI{})])p\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
    )
  THEN  BHyp  -1
  )

---

Home Index