---

Step * of Lemma pscm-presheaf-type-ap-morph

∀[A,I,J,f,a,u,s:Top].  ((u a f) ~ (u (s)a f))
BY
{ ((UnivCD THENA Auto) THEN RW  (SubC (SymbCompC [] 100)) 0 THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}[A,I,J,f,a,u,s:Top].    ((u  a  f)  \msim{}  (u  (s)a  f))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RW    (SubC  (SymbCompC  []  100))  0  THEN  EqCD)

---

Home Index