---

Step * of Lemma cubes-comp

∀[X:Top]. (cat-comp(cubes(X)) ~ λAa,Bb,_,f,g. g ⋅ f)
BY
{ PresheafMLTTInstance Obid: sets-comp⋅ }

---

Latex:

---

Latex:
\mforall{}[X:Top].  (cat-comp(cubes(X))  \msim{}  \mlambda{}Aa,Bb,$_{}$,f,g.  g  \mcdot{}  f)


By

---

Latex:
PresheafMLTTInstance  Obid:  sets-comp\mcdot{}

---

Home Index