---

Step * 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))
∧ (∀[m:?CubicalContext]. (bind-provision(m;u.OK(u)) = m ∈ ?CubicalContext))
∧ (∀[m:?CubicalContext]. ∀[f,g:CubicalContext ⟶ ?CubicalContext].
     (bind-provision(bind-provision(m;u.f u);u.g u) = bind-provision(m;u.bind-provision(f u;u.g u)) ∈ ?CubicalContext))
BY
{ D 0 }

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

2
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))
⊢ (∀[m:?CubicalContext]. (bind-provision(m;u.OK(u)) = m ∈ ?CubicalContext))
∧ (∀[m:?CubicalContext]. ∀[f,g:CubicalContext ⟶ ?CubicalContext].
     (bind-provision(bind-provision(m;u.f u);u.g u) = bind-provision(m;u.bind-provision(f u;u.g u)) ∈ ?CubicalContext))

---

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)))
\mwedge{}  (\mforall{}[m:?CubicalContext].  (bind-provision(m;u.OK(u))  =  m))
\mwedge{}  (\mforall{}[m:?CubicalContext].  \mforall{}[f,g:CubicalContext  {}\mrightarrow{}  ?CubicalContext].
          (bind-provision(bind-provision(m;u.f  u);u.g  u)
          =  bind-provision(m;u.bind-provision(f  u;u.g  u))))


By

---

Latex:
D  0

---

Home Index