---

Step * 1 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
⊢ λe.(↑e ∈b Ia) ←←= g1 o g2== λe.(↑e ∈b Ic)
BY
{ (NoLevelConstants ⌜Type⌝  (Using [`R',⌜λe.(↑e ∈b Ia)⌝; `Q', ⌜λe.(↑e ∈b Ib)⌝
    ] (BLemma `weak-antecedent-surjections-compose`))⋅
   THEN Reduce 0
   THEN Auto
   THEN Try ((Fold `es-E-interface` 0⋅ THEN Auto))) }

---

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
\mvdash{}  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1  o  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)


By

---

Latex:
(NoLevelConstants  \mkleeneopen{}Type\mkleeneclose{}    (Using  [`R',\mkleeneopen{}\mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)\mkleeneclose{};  `Q',  \mkleeneopen{}\mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)\mkleeneclose{}
    ]  (BLemma  `weak-antecedent-surjections-compose`))\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((Fold  `es-E-interface`  0\mcdot{}  THEN  Auto)))

---

Home Index