---

Step * 1 1 of Lemma quotient-dep-function-subtype


1. X : Type
2. X ⊆r Base
3. A : X ⟶ Type
4. E : x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ
5. ∀x:X. EquivRel(A[x];a,b.E[x;a;b])
6. ∀x:X. a,b:A[x]//E[x;a;b] ≡ a,b:A[x]//(↓E[x;a;b])
7. ∀x:X. EquivRel(A[x];a,b.↓E[x;a;b])
8. EquivRel(x:X ⟶ A[x];f,g.∀x:X. (↓E[x;f x;g x]))
⊢ (x:X ⟶ (a,b:A[x]//E[x;a;b])) ⊆r (f,g:x:X ⟶ A[x]//(∀x:X. (↓E[x;f x;g x])))
BY
{ TACTIC:((D 0 THENA Auto) THEN (GenConcl ⌜x = y ∈ (x:X ⟶ (a,b:A[x]//E[x;a;b]))⌝⋅ THENA Auto) THEN ThinVar `x') }

1
1. X : Type
2. X ⊆r Base
3. A : X ⟶ Type
4. E : x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ
5. ∀x:X. EquivRel(A[x];a,b.E[x;a;b])
6. ∀x:X. a,b:A[x]//E[x;a;b] ≡ a,b:A[x]//(↓E[x;a;b])
7. ∀x:X. EquivRel(A[x];a,b.↓E[x;a;b])
8. EquivRel(x:X ⟶ A[x];f,g.∀x:X. (↓E[x;f x;g x]))
9. y : x:X ⟶ (a,b:A[x]//E[x;a;b])
⊢ y ∈ f,g:x:X ⟶ A[x]//(∀x:X. (↓E[x;f x;g x]))

---

Latex:

---

Latex:

1.  X  :  Type
2.  X  \msubseteq{}r  Base
3.  A  :  X  {}\mrightarrow{}  Type
4.  E  :  x:X  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x:X.  EquivRel(A[x];a,b.E[x;a;b])
6.  \mforall{}x:X.  a,b:A[x]//E[x;a;b]  \mequiv{}  a,b:A[x]//(\mdownarrow{}E[x;a;b])
7.  \mforall{}x:X.  EquivRel(A[x];a,b.\mdownarrow{}E[x;a;b])
8.  EquivRel(x:X  {}\mrightarrow{}  A[x];f,g.\mforall{}x:X.  (\mdownarrow{}E[x;f  x;g  x]))
\mvdash{}  (x:X  {}\mrightarrow{}  (a,b:A[x]//E[x;a;b]))  \msubseteq{}r  (f,g:x:X  {}\mrightarrow{}  A[x]//(\mforall{}x:X.  (\mdownarrow{}E[x;f  x;g  x])))


By

---

Latex:
TACTIC:((D  0  THENA  Auto)  THEN  (GenConcl  \mkleeneopen{}x  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ThinVar  `x')

---

Home Index