---

Step * 1 of Lemma disjoint-quotient_subtype


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 ]))
BY
{ (D 3 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \mneg{}(A  \mwedge{}  B)
4.  E  :  (A  +  B)  {}\mrightarrow{}  (A  +  B)  {}\mrightarrow{}  \mBbbP{}
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]
\mvdash{}  (inr  y  )  =  (inl  x2)


By

---

Latex:
(D  3  THEN  Auto)

---

Home Index