---

Step * of Lemma glued-composes

∀[Info:Type]
  ∀es:EO+(Info)
    ∀[A,B,C:Type].
      ∀Ia:EClass(A). ∀Ib:EClass(B). ∀Ic:EClass(C). ∀f1:E(Ia) ─→ B. ∀f2:B ─→ C.
        ((glued(es;B;f1;Ia;Ib) ∧ glued(es;C;λe.(f2 Ib(e));Ib;Ic)) ⇒ glued(es;C;f2 o f1;Ia;Ic))
BY
{ (((Auto THEN All (Unfold `glued`)) THEN D -1) THEN D -3) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [A] : Type
4. [B] : Type
5. [C] : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. Ic : EClass(C)@i'
9. f1 : E(Ia) ─→ B@i
10. f2 : B ─→ C@i
11. g1 : E(Ib) ─→ E@i
12. g1 glues Ia ──f1─→ Ib@i
13. g : E(Ic) ─→ E@i
14. g glues Ib ──λe.(f2 Ib(e))─→ Ic@i
⊢ ∃g:E(Ic) ─→ E. g glues Ia ──f2 o f1─→ Ic

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A,B,C:Type].
            \mforall{}Ia:EClass(A).  \mforall{}Ib:EClass(B).  \mforall{}Ic:EClass(C).  \mforall{}f1:E(Ia)  {}\mrightarrow{}  B.  \mforall{}f2:B  {}\mrightarrow{}  C.
                ((glued(es;B;f1;Ia;Ib)  \mwedge{}  glued(es;C;\mlambda{}e.(f2  Ib(e));Ib;Ic))  {}\mRightarrow{}  glued(es;C;f2  o  f1;Ia;Ic))


By

---

Latex:
(((Auto  THEN  All  (Unfold  `glued`))  THEN  D  -1)  THEN  D  -3)

---

Home Index