---

Step * 3 of Lemma Q-R-glues-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(Ia)@i
15. g2 : E(Ic) ─→ E(Ib)@i
16. λe.(↑e ∈b Ia) ←←= g1== λe.(↑e ∈b Ib)@i
17. g1 is Qa-Rb-pre-preserving on λe.(↑e ∈b Ib)@i
18. Inj(E(Ib);E;g1)@i
19. ∀e:E(Ib). ((f1 (g1 e)) = Ib(e) ∈ B)@i
20. λe.(↑e ∈b Ib) ←←= g2== λe.(↑e ∈b Ic)@i
21. g2 is Rb-Sc-pre-preserving on λe.(↑e ∈b Ic)@i
22. Inj(E(Ic);E;g2)@i
23. ∀e:E(Ic). ((f2 Ib(g2 e)) = Ic(e) ∈ C)@i
24. λe.(↑e ∈b Ia) ←←= g1 o g2== λe.(↑e ∈b Ic)
25. g1 o g2 is Qa-Sc-pre-preserving on λe.(↑e ∈b Ic)
⊢ Inj(E(Ic);E;g1 o g2)
BY
{ RepUR ``compose`` 0 }

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(Ia)@i
15. g2 : E(Ic) ─→ E(Ib)@i
16. λe.(↑e ∈b Ia) ←←= g1== λe.(↑e ∈b Ib)@i
17. g1 is Qa-Rb-pre-preserving on λe.(↑e ∈b Ib)@i
18. Inj(E(Ib);E;g1)@i
19. ∀e:E(Ib). ((f1 (g1 e)) = Ib(e) ∈ B)@i
20. λe.(↑e ∈b Ib) ←←= g2== λe.(↑e ∈b Ic)@i
21. g2 is Rb-Sc-pre-preserving on λe.(↑e ∈b Ic)@i
22. Inj(E(Ic);E;g2)@i
23. ∀e:E(Ic). ((f2 Ib(g2 e)) = Ic(e) ∈ C)@i
24. λe.(↑e ∈b Ia) ←←= g1 o g2== λe.(↑e ∈b Ic)
25. g1 o g2 is Qa-Sc-pre-preserving on λe.(↑e ∈b Ic)
⊢ Inj(E(Ic);E;λx.(g1 (g2 x)))

---

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(Ia)@i
15.  g2  :  E(Ic)  {}\mrightarrow{}  E(Ib)@i
16.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
17.  g1  is  Qa-Rb-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
18.  Inj(E(Ib);E;g1)@i
19.  \mforall{}e:E(Ib).  ((f1  (g1  e))  =  Ib(e))@i
20.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)  \mleftarrow{}\mleftarrow{}=  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
21.  g2  is  Rb-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
22.  Inj(E(Ic);E;g2)@i
23.  \mforall{}e:E(Ic).  ((f2  Ib(g2  e))  =  Ic(e))@i
24.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1  o  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)
25.  g1  o  g2  is  Qa-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)
\mvdash{}  Inj(E(Ic);E;g1  o  g2)


By

---

Latex:
RepUR  ``compose``  0

---

Home Index