Step
*
2
3
1
of Lemma
equipollent-quotient
.....aux.....
1. A : Type
2. E : A ⟶ A ⟶ 𝔹
3. EquivRel(A;x,y.↑(E x y))
4. E ∈ (x,y:A//(↑(E x y))) ⟶ A ⟶ 𝔹
5. Refl(A;x,y.↑(E x y))
6. Sym(A;x,y.↑(E x y))
7. Trans(A;x,y.↑(E x y))
8. f : A ⟶ (a:x,y:A//(↑(E x y)) × {b:A| ↑(E a b)} )
⊢ x,y:A//(↑(E x y)) ∈ Type
BY
{ MemCD
THEN Thin 4
THEN Auto }
Latex:
Latex:
.....aux.....
1. A : Type
2. E : A {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{}
3. EquivRel(A;x,y.\muparrow{}(E x y))
4. E \mmember{} (x,y:A//(\muparrow{}(E x y))) {}\mrightarrow{} A {}\mrightarrow{} \mBbbB{}
5. Refl(A;x,y.\muparrow{}(E x y))
6. Sym(A;x,y.\muparrow{}(E x y))
7. Trans(A;x,y.\muparrow{}(E x y))
8. f : A {}\mrightarrow{} (a:x,y:A//(\muparrow{}(E x y)) \mtimes{} \{b:A| \muparrow{}(E a b)\} )
\mvdash{} x,y:A//(\muparrow{}(E x y)) \mmember{} Type
By
Latex:
MemCD
THEN Thin 4
THEN Auto
Home
Index