---

Step * of Lemma glue-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. ∀g1:E(Ib) ─→ E. ∀g2:E(Ic) ─→ E.
        ((g1 glues Ia ──f1─→ Ib ∧ g2 glues Ib ──λe.(f2 Ib(e))─→ Ic) ⇒ g1 o g2 glues Ia ──f2 o f1─→ Ic)
BY
{ (Auto THEN All (Unfold `glues`)) }

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. g2 : E(Ic) ─→ E@i
13. g1 glues Ia:λe,e'. e ≤loc e'  ──f1─→ Ib:λe,e'. e ≤loc e' @i
14. g2 glues Ib:λe,e'. e ≤loc e'  ──λe.(f2 Ib(e))─→ Ic:λe,e'. e ≤loc e' @i
⊢ g1 o g2 glues Ia:λe,e'. e ≤loc e'  ──f2 o f1─→ Ic:λe,e'. e ≤loc e' 

---

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.  \mforall{}g1:E(Ib)  {}\mrightarrow{}  E.
            \mforall{}g2:E(Ic)  {}\mrightarrow{}  E.
                ((g1  glues  Ia  {}{}f1{}\mrightarrow{}  Ib  \mwedge{}  g2  glues  Ib  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic)
                {}\mRightarrow{}  g1  o  g2  glues  Ia  {}{}f2  o  f1{}\mrightarrow{}  Ic)


By

---

Latex:
(Auto  THEN  All  (Unfold  `glues`))

---

Home Index