---

Step * 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:λ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' 
BY
{ (Using [`Ib',⌈Ib⌉;`Rb',⌈λe,e'. e ≤loc e' ⌉] (BLemma `Q-R-glues-composes`)⋅
   THEN Try (Complete (Auto))
   THEN All (Fold `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 ──f1─→ Ib@i
14. g2 glues Ib ──λe.(f2 Ib(e))─→ Ic@i
⊢ g1 ∈ E(Ib) ─→ E(Ia)

2
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
⊢ g2 ∈ E(Ic) ─→ E(Ib)

---

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:\mlambda{}e,e'.  e  \mleq{}loc  e'    {}{}f1{}\mrightarrow{}  Ib:\mlambda{}e,e'.  e  \mleq{}loc  e'  @i
14.  g2  glues  Ib:\mlambda{}e,e'.  e  \mleq{}loc  e'    {}{}\mlambda{}e.(f2  Ib(e)){}\mrightarrow{}  Ic:\mlambda{}e,e'.  e  \mleq{}loc  e'  @i
\mvdash{}  g1  o  g2  glues  Ia:\mlambda{}e,e'.  e  \mleq{}loc  e'    {}{}f2  o  f1{}\mrightarrow{}  Ic:\mlambda{}e,e'.  e  \mleq{}loc  e' 


By

---

Latex:
(Using  [`Ib',\mkleeneopen{}Ib\mkleeneclose{};`Rb',\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{}]  (BLemma  `Q-R-glues-composes`)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  All  (Fold  `glues`))

---

Home Index