---

Step * of Lemma cubes-arrow

∀[X:Top]. (cat-arrow(cubes(X)) ~ λAa,Bb. let A,a = Aa in let B,b = Bb in {f:A ⟶ B| f(b) = a ∈ (X A)} )
BY
{ PresheafMLTTInstance Obid: sets-arrow⋅ }

---

Latex:

---

Latex:
\mforall{}[X:Top].  (cat-arrow(cubes(X))  \msim{}  \mlambda{}Aa,Bb.  let  A,a  =  Aa  in  let  B,b  =  Bb  in  \{f:A  {}\mrightarrow{}  B|  f(b)  =  a\}  )


By

---

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

---

Home Index