---

Step * 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])
⊢ (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:(Assert EquivRel(x:X ⟶ A[x];f,g.∀x:X. (↓E[x;f x;g x])) BY
                ((D 0 THEN Auto)
                 THEN D 0
                 THEN Reduce 0
                 THEN Auto
                 THEN RepeatFor 2 ((InstHyp [⌜x⌝] (-3)⋅ THENA Auto))
                 THEN (InstHyp [⌜x⌝] 7⋅ THENA Auto)
                 THEN UseTrans ⌜b 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]))
⊢ (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])))

---

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])
\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:(Assert  EquivRel(x:X  {}\mrightarrow{}  A[x];f,g.\mforall{}x:X.  (\mdownarrow{}E[x;f  x;g  x]))  BY
                            ((D  0  THEN  Auto)
                              THEN  D  0
                              THEN  Reduce  0
                              THEN  Auto
                              THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
                              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
                              THEN  UseTrans  \mkleeneopen{}b  x\mkleeneclose{}\mcdot{}))

---

Home Index