---

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

No Annotations
(∀[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
{ (InstLemma `provisional-monad_wf` [⌜parm{i''''}⌝]⋅
   THEN RepUR ``provisional-monad monad mk_monad`` -1
   THEN RepeatFor 5 (((MemHD (-1) THENA Auto) THEN All Reduce THEN All (Fold `member`)))) }

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))
∧ (∀[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:
No  Annotations
(\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:
(InstLemma  `provisional-monad\_wf`  [\mkleeneopen{}parm\{i''''\}\mkleeneclose{}]\mcdot{}
  THEN  RepUR  ``provisional-monad  monad  mk\_monad``  -1
  THEN  RepeatFor  5  (((MemHD  (-1)  THENA  Auto)  THEN  All  Reduce  THEN  All  (Fold  `member`))))

---

Home Index