---

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