Step
*
1
2
1
1
of Lemma
equipollent-quotient2
1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A. Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A. (isl(d x y) ∈ 𝔹)
6. ∀x,y:A. (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} ∈ Type
⊢ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ~ a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)}
BY
{ (Using [`f',⌜λx.x⌝] (BLemma `product_functionality_wrt_equipollent_dependent`)⋅ THENA Try (Complete (Auto))) }
1
.....wf.....
1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A. Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A. (isl(d x y) ∈ 𝔹)
6. ∀x,y:A. (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} ∈ Type
⊢ λa.{b:A| ↑isl(d a b)} ∈ (x,y:A//(↑isl(d x y))) ⟶ Type
2
.....wf.....
1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A. Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A. (isl(d x y) ∈ 𝔹)
6. ∀x,y:A. (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} ∈ Type
⊢ λa.{b:A| ↑isl(d a b)} ∈ (x,y:A//(↓E[x;y])) ⟶ Type
3
1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A. Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A. (isl(d x y) ∈ 𝔹)
6. ∀x,y:A. (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} ∈ Type
⊢ Bij(x,y:A//(↑isl(d x y));x,y:A//(↓E[x;y]);λx.x)
4
1. [A] : Type
2. E : A ⟶ A ⟶ ℙ
3. d : ∀x,y:A. Dec(↓E[x;y])
4. EquivRel(A;x,y.↓E[x;y])
5. ∀x,y:A. (isl(d x y) ∈ 𝔹)
6. ∀x,y:A. (↑isl(d x y) ⇐⇒ ↓E[x;y])
7. A ~ a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)}
8. EquivRel(A;x,y.↑isl(d x y))
9. x,y:A//(↓E[x;y]) ≡ x,y:A//(↑isl(d x y))
10. a:x,y:A//(↑isl(d x y)) × {b:A| ↑isl(d a b)} ∈ Type
11. a:x,y:A//(↓E[x;y]) × {b:A| ↑isl(d a b)} ∈ Type
⊢ ∀a:x,y:A//(↑isl(d x y)). {b:A| ↑isl(d a b)} ~ {b:A| ↑isl(d ((λx.x) a) b)}
Latex:
Latex:
1. [A] : Type
2. E : A {}\mrightarrow{} A {}\mrightarrow{} \mBbbP{}
3. d : \mforall{}x,y:A. Dec(\mdownarrow{}E[x;y])
4. EquivRel(A;x,y.\mdownarrow{}E[x;y])
5. \mforall{}x,y:A. (isl(d x y) \mmember{} \mBbbB{})
6. \mforall{}x,y:A. (\muparrow{}isl(d x y) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}E[x;y])
7. A \msim{} a:x,y:A//(\muparrow{}isl(d x y)) \mtimes{} \{b:A| \muparrow{}isl(d a b)\}
8. EquivRel(A;x,y.\muparrow{}isl(d x y))
9. x,y:A//(\mdownarrow{}E[x;y]) \mequiv{} x,y:A//(\muparrow{}isl(d x y))
10. a:x,y:A//(\muparrow{}isl(d x y)) \mtimes{} \{b:A| \muparrow{}isl(d a b)\} \mmember{} Type
11. a:x,y:A//(\mdownarrow{}E[x;y]) \mtimes{} \{b:A| \muparrow{}isl(d a b)\} \mmember{} Type
\mvdash{} a:x,y:A//(\muparrow{}isl(d x y)) \mtimes{} \{b:A| \muparrow{}isl(d a b)\} \msim{} a:x,y:A//(\mdownarrow{}E[x;y]) \mtimes{} \{b:A| \muparrow{}isl(d a b)\}
By
Latex:
(Using [`f',\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}] (BLemma `product\_functionality\_wrt\_equipollent\_dependent`)\mcdot{}
THENA Try (Complete (Auto))
)
Home
Index