---

Step * of Lemma quotient-dep-function-subtype

∀[X:Type]
  ∀[A:X ⟶ Type]. ∀[E:x:X ⟶ A[x] ⟶ A[x] ⟶ ℙ].
    ((∀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]))))) 
  supposing X ⊆r Base
BY
{ TACTIC:(Auto
          THEN (Assert ∀x:X. a,b:A[x]//E[x;a;b] ≡ a,b:A[x]//(↓E[x;a;b]) BY
                      (Auto THEN BLemma `quotient-squash` THEN Auto))
          THEN (Assert ∀x:X. EquivRel(A[x];a,b.↓E[x;a;b]) BY
                      (ParallelOp -2 THEN BLemma `equiv_rel_squash` THEN Auto))) }

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])
⊢ (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:
\mforall{}[X:Type]
    \mforall{}[A:X  {}\mrightarrow{}  Type].  \mforall{}[E:x:X  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  A[x]  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}x:X.  EquivRel(A[x];a,b.E[x;a;b]))
        {}\mRightarrow{}  ((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]))))) 
    supposing  X  \msubseteq{}r  Base


By

---

Latex:
TACTIC:(Auto
                THEN  (Assert  \mforall{}x:X.  a,b:A[x]//E[x;a;b]  \mequiv{}  a,b:A[x]//(\mdownarrow{}E[x;a;b])  BY
                                        (Auto  THEN  BLemma  `quotient-squash`  THEN  Auto))
                THEN  (Assert  \mforall{}x:X.  EquivRel(A[x];a,b.\mdownarrow{}E[x;a;b])  BY
                                        (ParallelOp  -2  THEN  BLemma  `equiv\_rel\_squash`  THEN  Auto)))

---

Home Index