---

Step * 1 1 of Lemma bind-provision-cubical-context-equations


1. λT.Provisional''''(T) ∈ 𝕌{i'''''} ⟶ 𝕌{i'''''}
2. λx.OK(x) ∈ ⋂T:𝕌{i'''''}. (T ⟶ Provisional''''(T))
3. λx,f. bind-provision(x;u.f u) ∈ ⋂T,S:𝕌{i'''''}.  (Provisional''''(T) ⟶ (T ⟶ Provisional''''(S)) ⟶ Provisional''''(\000CS))
4. Ax ∈ ∀[T,S:𝕌{i'''''}]. ∀[x:T]. ∀[f:T ⟶ Provisional''''(S)].
          (bind-provision(OK(x);u.f u) = (f x) ∈ Provisional''''(S))
5. Ax ∈ ∀[T:𝕌{i'''''}]. ∀[m:Provisional''''(T)].  (bind-provision(m;u.OK(u)) = m ∈ Provisional''''(T))
6. Ax ∈ ∀[T,S,U:𝕌{i'''''}]. ∀[m:Provisional''''(T)]. ∀[f:T ⟶ Provisional''''(S)]. ∀[g:S ⟶ Provisional''''(U)].
          (bind-provision(bind-provision(m;u.f u);u.g u)
          = bind-provision(m;u.bind-provision(f u;u.g u))
          ∈ Provisional''''(U))
⊢ ∀[x:CubicalContext]. ∀[f:CubicalContext ⟶ ?CubicalContext].  (bind-provision(OK(x);u.f u) = (f x) ∈ ?CubicalContext)
BY
{ ((Assert ∀[T,S:𝕌{i'''''}]. ∀[x:T]. ∀[f:T ⟶ Provisional''''(S)].
             (bind-provision(OK(x);u.f u) = (f x) ∈ Provisional''''(S)) BY
          (UseWitness ⌜Ax⌝⋅ THEN Trivial))
   THEN RepeatFor 2 ((D -1 With ⌜CubicalContext⌝  THENA Auto))
   THEN Fold `cubical-context` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:

1.  \mlambda{}T.Provisional''''(T)  \mmember{}  \mBbbU{}\{i'''''\}  {}\mrightarrow{}  \mBbbU{}\{i'''''\}
2.  \mlambda{}x.OK(x)  \mmember{}  \mcap{}T:\mBbbU{}\{i'''''\}.  (T  {}\mrightarrow{}  Provisional''''(T))
3.  \mlambda{}x,f.  bind-provision(x;u.f  u)  \mmember{}  \mcap{}T,S:\mBbbU{}\{i'''''\}.
                                                                  (Provisional''''(T)
                                                                  {}\mrightarrow{}  (T  {}\mrightarrow{}  Provisional''''(S))
                                                                  {}\mrightarrow{}  Provisional''''(S))
4.  Ax  \mmember{}  \mforall{}[T,S:\mBbbU{}\{i'''''\}].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  Provisional''''(S)].
                    (bind-provision(OK(x);u.f  u)  =  (f  x))
5.  Ax  \mmember{}  \mforall{}[T:\mBbbU{}\{i'''''\}].  \mforall{}[m:Provisional''''(T)].    (bind-provision(m;u.OK(u))  =  m)
6.  Ax  \mmember{}  \mforall{}[T,S,U:\mBbbU{}\{i'''''\}].  \mforall{}[m:Provisional''''(T)].  \mforall{}[f:T  {}\mrightarrow{}  Provisional''''(S)].
                \mforall{}[g:S  {}\mrightarrow{}  Provisional''''(U)].
                    (bind-provision(bind-provision(m;u.f  u);u.g  u)
                    =  bind-provision(m;u.bind-provision(f  u;u.g  u)))
\mvdash{}  \mforall{}[x:CubicalContext].  \mforall{}[f:CubicalContext  {}\mrightarrow{}  ?CubicalContext].
        (bind-provision(OK(x);u.f  u)  =  (f  x))


By

---

Latex:
((Assert  \mforall{}[T,S:\mBbbU{}\{i'''''\}].  \mforall{}[x:T].  \mforall{}[f:T  {}\mrightarrow{}  Provisional''''(S)].
                      (bind-provision(OK(x);u.f  u)  =  (f  x))  BY
                (UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Trivial))
  THEN  RepeatFor  2  ((D  -1  With  \mkleeneopen{}CubicalContext\mkleeneclose{}    THENA  Auto))
  THEN  Fold  `cubical-context`  (-1)
  THEN  Trivial)

---

Home Index