---

Step * of Lemma disjoint-quotient_subtype

∀[A,B:Type].
  ∀[E:(A + B) ⟶ (A + B) ⟶ ℙ]
    (x,y:A + B//E[x;y]) ⊆r (a1,a2:A//E[inl a1;inl a2] + (b1,b2:B//E[inr b1 ;inr b2 ])) 
    supposing EquivRel(A + B;x,y.E[x;y]) 
  supposing ¬(A ∧ B)
BY
{ (Auto
   THEN (Assert EquivRel(A;x,y.E[inl x;inl y]) BY
               (RepeatFor 3 (ParallelLast) THEN Auto THEN ParallelLast THEN Auto))
   THEN (Assert EquivRel(B;x,y.E[inr x ;inr y ]) BY
               (RepeatFor 3 (ParallelOp -2) THEN Auto THEN ParallelOp -2 THEN Auto))
   THEN (D 0 THENA Auto)
   THEN quotD (-1)
   THEN Auto
   THEN DProdsAndUnions
   THEN Try (EqCD)
   THEN Auto) }

1
1. A : Type
2. B : Type
3. ¬(A ∧ B)
4. E : (A + B) ⟶ (A + B) ⟶ ℙ
5. EquivRel(A + B;x,y.E[x;y])
6. EquivRel(A;x,y.E[inl x;inl y])
7. EquivRel(B;x,y.E[inr x ;inr y ])
8. y : B
9. x2 : A
10. E[inr y ;inl x2]
⊢ (inr y ) = (inl x2) ∈ (a1,a2:A//E[inl a1;inl a2] + (b1,b2:B//E[inr b1 ;inr b2 ]))

2
1. A : Type
2. B : Type
3. ¬(A ∧ B)
4. E : (A + B) ⟶ (A + B) ⟶ ℙ
5. EquivRel(A + B;x,y.E[x;y])
6. EquivRel(A;x,y.E[inl x;inl y])
7. EquivRel(B;x,y.E[inr x ;inr y ])
8. x1 : A
9. y : B
10. E[inl x1;inr y ]
⊢ (inl x1) = (inr y ) ∈ (a1,a2:A//E[inl a1;inl a2] + (b1,b2:B//E[inr b1 ;inr b2 ]))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[E:(A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbP{}]
        (x,y:A  +  B//E[x;y])  \msubseteq{}r  (a1,a2:A//E[inl  a1;inl  a2]  +  (b1,b2:B//E[inr  b1  ;inr  b2  ])) 
        supposing  EquivRel(A  +  B;x,y.E[x;y]) 
    supposing  \mneg{}(A  \mwedge{}  B)


By

---

Latex:
(Auto
  THEN  (Assert  EquivRel(A;x,y.E[inl  x;inl  y])  BY
                          (RepeatFor  3  (ParallelLast)  THEN  Auto  THEN  ParallelLast  THEN  Auto))
  THEN  (Assert  EquivRel(B;x,y.E[inr  x  ;inr  y  ])  BY
                          (RepeatFor  3  (ParallelOp  -2)  THEN  Auto  THEN  ParallelOp  -2  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  quotD  (-1)
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  Try  (EqCD)
  THEN  Auto)

---

Home Index