---

Step * 2 of Lemma fill-type-up_wf


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)}
BY
{ ((InferEqualType THEN Try (Trivial))
   THEN (InstLemma `cubical-fun-as-cubical-pi` [⌜Gamma.𝕀⌝;⌜((A)[0(𝕀)])p⌝;⌜A⌝]⋅ THENA Auto)
   THEN EqCDA
   THEN Auto) }

---

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.  fill-type-up(Gamma;A;cA)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:\mPi{}((A)[0(\mBbbI{})])p  (A)p\}
\mvdash{}  fill-type-up(Gamma;A;cA)  \mmember{}  \{Gamma.\mBbbI{}  \mvdash{}  \_:(((A)[0(\mBbbI{})])p  {}\mrightarrow{}  A)\}


By

---

Latex:
((InferEqualType  THEN  Try  (Trivial))
  THEN  (InstLemma  `cubical-fun-as-cubical-pi`  [\mkleeneopen{}Gamma.\mBbbI{}\mkleeneclose{};\mkleeneopen{}((A)[0(\mBbbI{})])p\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  EqCDA
  THEN  Auto)

---

Home Index