---

Step * of Lemma csm-fiber-comp

No Annotations
∀[G:j⊢]. ∀[A,T:{G ⊢ _}]. ∀[a:{G ⊢ _:A}]. ∀[cA:G +⊢ Compositon(A)]. ∀[cT:G ⊢ Compositon(T)]. ∀[H:j⊢]. ∀[s:H j⟶ G].
∀[f:{G ⊢ _:(T ⟶ A)}].
  ((fiber-comp(G;T;A;f;a;cT;cA))s = fiber-comp(H;(T)s;(A)s;(f)s;(a)s;(cT)s;(cA)s) ∈ H ⊢ Compositon(Fiber((f)s;(a)s)))
BY
{ (Intros THEN RWO "csm-fiber-comp-sq" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].  \mforall{}[cA:G  +\mvdash{}  Compositon(A)].  \mforall{}[cT:G  \mvdash{}  Compositon(T)].  \mforall{}[H:j\mvdash{}].
\mforall{}[s:H  j{}\mrightarrow{}  G].  \mforall{}[f:\{G  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}].
    ((fiber-comp(G;T;A;f;a;cT;cA))s  =  fiber-comp(H;(T)s;(A)s;(f)s;(a)s;(cT)s;(cA)s))


By

---

Latex:
(Intros  THEN  RWO  "csm-fiber-comp-sq"  0  THEN  Auto)

---

Home Index