---

Step * of Lemma glue-comp_wf3

No Annotations
∀G:j⊢. ∀A:{G ⊢ _}. ∀cA:G +⊢ Compositon(A). ∀psi:{G ⊢ _:𝔽}. ∀T:{G, psi ⊢ _}. ∀cT:G, psi +⊢ Compositon(T).
∀f:{G, psi ⊢ _:Equiv(T;A)}.
  (comp(Glue [psi ⊢→ (T, f)] A)  ∈ G ⊢ Compositon(gluetype(G;A;psi;T;f)))
BY
{ (InstLemma `glue-comp_wf2` [] THEN Fold `gluetype` (-1) THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}G:j\mvdash{}.  \mforall{}A:\{G  \mvdash{}  \_\}.  \mforall{}cA:G  +\mvdash{}  Compositon(A).  \mforall{}psi:\{G  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}T:\{G,  psi  \mvdash{}  \_\}.
\mforall{}cT:G,  psi  +\mvdash{}  Compositon(T).  \mforall{}f:\{G,  psi  \mvdash{}  \_:Equiv(T;A)\}.
    (comp(Glue  [psi  \mvdash{}\mrightarrow{}  (T,  f)]  A)    \mmember{}  G  \mvdash{}  Compositon(gluetype(G;A;psi;T;f)))


By

---

Latex:
(InstLemma  `glue-comp\_wf2`  []  THEN  Fold  `gluetype`  (-1)  THEN  Trivial)

---

Home Index