---

Step * of Lemma Q-R-glued-composes

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

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

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[Qa,Rb,Sc:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].  \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.
                ((Ia:Qa  \mrightarrow{}{}f1{}\mrightarrow{}    Ib:Rb  \mwedge{}  Ib:Rb  \mrightarrow{}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}    Ic:Sc)  {}\mRightarrow{}  Ia:Qa  \mrightarrow{}{}f2  o  f1{}\mrightarrow{}    Ic:Sc)


By

---

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

---

Home Index