Step * 1 1 2 of Lemma equiv-equipollent-iff-quotient-equipollent


1. Type
2. Type
3. A ⟶ A ⟶ ℙ
4. EquivRel(A;x,y.E[x;y])
5. (x,y:A//E[x;y]) ⟶ A
6. ∀c:x,y:A//E[x;y]. ((g c) c ∈ (x,y:A//E[x;y]))
7. (x,y:A//E[x;y]) ⟶ B
8. Inj(x,y:A//E[x;y];B;f)
9. Surj(x,y:A//E[x;y];B;f)
10. Surj(A;B;f)
11. a1 A
12. a2 A
13. (f a1) (f a2) ∈ B
⊢ ↓E[a1;a2]
BY
((Assert a1 a2 ∈ (x,y:A//E[x;y]) BY Auto) THEN EqTypeHD (-1) THEN Auto) }


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  E  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  EquivRel(A;x,y.E[x;y])
5.  g  :  (x,y:A//E[x;y])  {}\mrightarrow{}  A
6.  \mforall{}c:x,y:A//E[x;y].  ((g  c)  =  c)
7.  f  :  (x,y:A//E[x;y])  {}\mrightarrow{}  B
8.  Inj(x,y:A//E[x;y];B;f)
9.  Surj(x,y:A//E[x;y];B;f)
10.  Surj(A;B;f)
11.  a1  :  A
12.  a2  :  A
13.  (f  a1)  =  (f  a2)
\mvdash{}  \mdownarrow{}E[a1;a2]


By


Latex:
((Assert  a1  =  a2  BY  Auto)  THEN  EqTypeHD  (-1)  THEN  Auto)




Home Index