---

Step * 1 1 of Lemma glued-composes


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

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
15. g ∈ E(Ic) ─→ E(Ib)
16. g1 ∈ E(Ib) ─→ E(Ia)
⊢ g1 o g glues Ia ──f2 o f1─→ Ic

---

Latex:

---

Latex:

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)  {}\mrightarrow{}  B@i
10.  f2  :  B  {}\mrightarrow{}  C@i
11.  g1  :  E(Ib)  {}\mrightarrow{}  E@i
12.  g1  glues  Ia  {}{}f1{}\mrightarrow{}  Ib@i
13.  g  :  E(Ic)  {}\mrightarrow{}  E@i
14.  g  glues  Ib  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic@i
15.  g  \mmember{}  E(Ic)  {}\mrightarrow{}  E(Ib)
16.  g1  \mmember{}  E(Ib)  {}\mrightarrow{}  E(Ia)
\mvdash{}  \mexists{}g:E(Ic)  {}\mrightarrow{}  E.  g  glues  Ia  {}{}f2  o  f1{}\mrightarrow{}  Ic


By

---

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

---

Home Index