---

Step * of Lemma fill-type-up_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ CompOp(A)].
  (fill-type-up(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:(((A)[0(𝕀)])p ⟶ A)})
BY
{ ((Intros THEN (Assert Gamma.𝕀 ⊢ ((A)[0(𝕀)])p BY Auto))
   THEN Assert ⌜fill-type-up(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p}⌝⋅
   ) }

1
.....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}

2
1. [Gamma] : CubicalSet{j}
2. [A] : {Gamma.𝕀 ⊢ _}
3. [cA] : Gamma.𝕀 ⊢ CompOp(A)
4. Gamma.𝕀 ⊢ ((A)[0(𝕀)])p
5. fill-type-up(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:Π((A)[0(𝕀)])p (A)p}
⊢ fill-type-up(Gamma;A;cA) ∈ {Gamma.𝕀 ⊢ _:(((A)[0(𝕀)])p ⟶ A)}

---

Latex:

---

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


By

---

Latex:
((Intros  THEN  (Assert  Gamma.\mBbbI{}  \mvdash{}  ((A)[0(\mBbbI{})])p  BY  Auto))
  THEN  Assert  \mkleeneopen{}fill-type-up(Gamma;A;cA)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:\mPi{}((A)[0(\mBbbI{})])p  (A)p\}\mkleeneclose{}\mcdot{}
  )

---

Home Index