---

Step * of Lemma cubical-universe-ap-morph

No Annotations
∀[I,b,J,f,a:Top].  ((b a f) ~ csm-fibrant-type(formal-cube(I);formal-cube(J);<f>;b))
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I,b,J,f,a:Top].    ((b  a  f)  \msim{}  csm-fibrant-type(formal-cube(I);formal-cube(J);<f>b))


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index