---

Step * of Lemma cubical_set-ext

No Annotations
{FM:F:fset(ℕ) ⟶ 𝕌{j'} × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ J ⟶ I ⟶ (F I) ⟶ (F J))| 
 let F,M = FM 
 in (∀I:fset(ℕ). ∀s:FM(I).  (1(s) = s ∈ FM(I)))
    ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀s:FM(I).  (f ⋅ g(s) = g(f(s)) ∈ FM(K)))}  ≡ CubicalSet{j}
BY
{ PresheafMLTTInstance Obid: ps_context-ext⋅ }

---

Latex:

---

Latex:
No  Annotations
\{FM:F:fset(\mBbbN{})  {}\mrightarrow{}  \mBbbU{}\{j'\}  \mtimes{}  (I:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  J  {}\mrightarrow{}  I  {}\mrightarrow{}  (F  I)  {}\mrightarrow{}  (F  J))| 
  let  F,M  =  FM 
  in  (\mforall{}I:fset(\mBbbN{}).  \mforall{}s:FM(I).    (1(s)  =  s))
        \mwedge{}  (\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}s:FM(I).    (f  \mcdot{}  g(s)  =  g(f(s))))\}    \mequiv{}  CubicalSet\{j\}


By

---

Latex:
PresheafMLTTInstance  Obid:  ps\_context-ext\mcdot{}

---

Home Index