---

Step * 1 1 of Lemma Q-R-glued-composes


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
18. g ∈ E(Ic) ─→ E(Ib)
19. g1 ∈ E(Ib) ─→ E(Ia)
⊢ ∃g:E(Ic) ─→ E. g glues Ia:Qa ──f2 o f1─→ Ic:Sc
BY
{ ((InstConcl [⌈g1 o g⌉])⋅ THENA Auto) }

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
18. g ∈ E(Ic) ─→ E(Ib)
19. g1 ∈ E(Ib) ─→ E(Ia)
⊢ g1 o g glues Ia:Qa ──f2 o f1─→ Ic:Sc

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [Qa]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  [Rb]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [Sc]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
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)  {}\mrightarrow{}  B@i
13.  f2  :  B  {}\mrightarrow{}  C@i
14.  g1  :  E(Ib)  {}\mrightarrow{}  E@i
15.  g1  glues  Ia:Qa  {}{}f1{}\mrightarrow{}  Ib:Rb@i
16.  g  :  E(Ic)  {}\mrightarrow{}  E@i
17.  g  glues  Ib:Rb  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic:Sc@i
18.  g  \mmember{}  E(Ic)  {}\mrightarrow{}  E(Ib)
19.  g1  \mmember{}  E(Ib)  {}\mrightarrow{}  E(Ia)
\mvdash{}  \mexists{}g:E(Ic)  {}\mrightarrow{}  E.  g  glues  Ia:Qa  {}{}f2  o  f1{}\mrightarrow{}  Ic:Sc


By

---

Latex:
((InstConcl  [\mkleeneopen{}g1  o  g\mkleeneclose{}])\mcdot{}  THENA  Auto)

---

Home Index