Step
*
of Lemma
Q-R-glues-conditional
∀[Info:Type]
∀es:EO+(Info)
∀[Q1,Q2,R:E ─→ E ─→ ℙ]. ∀[A,B:Type].
∀Ia1,Ia2:EClass(A). ∀Ib1,Ib2:EClass(B). ∀f:E([Ia1?Ia2]) ─→ B. ∀g1:E(Ib1) ─→ E(Ia1). ∀g2:E(Ib2) ─→ E(Ia2).
(g1 glues Ia1:Q1 ──f─→ Ib1:R
⇒ g2 glues Ia2:Q2 ──f─→ Ib2:R
⇒ [{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R) supposing
(Ib1 ∩ Ib2 = 0 and
Ia1 ∩ Ia2 = 0)
BY
{ Auto }
1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [Q1] : E ─→ E ─→ ℙ
4. [Q2] : E ─→ E ─→ ℙ
5. [R] : E ─→ E ─→ ℙ
6. [A] : Type
7. [B] : Type
8. Ia1 : EClass(A)@i'
9. Ia2 : EClass(A)@i'
10. Ib1 : EClass(B)@i'
11. Ib2 : EClass(B)@i'
12. f : E([Ia1?Ia2]) ─→ B@i
13. g1 : E(Ib1) ─→ E(Ia1)@i
14. g2 : E(Ib2) ─→ E(Ia2)@i
15. Ia1 ∩ Ia2 = 0
16. Ib1 ∩ Ib2 = 0
17. g1 glues Ia1:Q1 ──f─→ Ib1:R@i
18. g2 glues Ia2:Q2 ──f─→ Ib2:R@i
⊢ [{Ib1}? g1 : g2] glues [Ia1?Ia2]:Q1|{Ia1} ∨ Q2|{Ia2} ──f─→ [Ib1?Ib2]:R
Latex:
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[Q1,Q2,R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}]. \mforall{}[A,B:Type].
\mforall{}Ia1,Ia2:EClass(A). \mforall{}Ib1,Ib2:EClass(B). \mforall{}f:E([Ia1?Ia2]) {}\mrightarrow{} B. \mforall{}g1:E(Ib1) {}\mrightarrow{} E(Ia1).
\mforall{}g2:E(Ib2) {}\mrightarrow{} E(Ia2).
(g1 glues Ia1:Q1 {}{}f{}\mrightarrow{} Ib1:R
{}\mRightarrow{} g2 glues Ia2:Q2 {}{}f{}\mrightarrow{} Ib2:R
{}\mRightarrow{} [\{Ib1\}? g1 : g2] glues [Ia1?Ia2]:Q1|\{Ia1\} \mvee{} Q2|\{Ia2\} {}{}f{}\mrightarrow{} [Ib1?Ib2]:R) supposing
(Ib1 \mcap{} Ib2 = 0 and
Ia1 \mcap{} Ia2 = 0)
By
Latex:
Auto
Home
Index