---

Step * 1 1 of Lemma glue-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. g2 : E(Ic) ─→ E@i
13. g1 glues Ia ──f1─→ Ib@i
14. g2 glues Ib ──λe.(f2 Ib(e))─→ Ic@i
⊢ g1 ∈ E(Ib) ─→ E(Ia)
BY
{ (FLemma `glues-property` [-2] THEN Auto) }

---

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.  g2  :  E(Ic)  {}\mrightarrow{}  E@i
13.  g1  glues  Ia  {}{}f1{}\mrightarrow{}  Ib@i
14.  g2  glues  Ib  {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic@i
\mvdash{}  g1  \mmember{}  E(Ib)  {}\mrightarrow{}  E(Ia)


By

---

Latex:
(FLemma  `glues-property`  [-2]  THEN  Auto)

---

Home Index