---

Step * of Lemma quotient-function-subtype

∀[X:Type]
  ∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
    (EquivRel(A;a,b.E[a;b]) ⇒ ((X ⟶ (a,b:A//E[a;b])) ⊆r (f,g:X ⟶ A//fun-equiv(X;a,b.↓E[a;b];f;g)))) 
  supposing X ⊆r Base
BY
{ (InstLemma `quotient-dep-function-subtype` []
   THEN (ParallelLast' THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA Auto)
   THEN Auto
   THEN InstHyp [⌜λ2x.A⌝;⌜λx,a,b. E[a;b]⌝] 3⋅
   THEN Auto
   THEN All (RepUR ``so_apply``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
        (EquivRel(A;a,b.E[a;b])
        {}\mRightarrow{}  ((X  {}\mrightarrow{}  (a,b:A//E[a;b]))  \msubseteq{}r  (f,g:X  {}\mrightarrow{}  A//fun-equiv(X;a,b.\mdownarrow{}E[a;b];f;g)))) 
    supposing  X  \msubseteq{}r  Base


By

---

Latex:
(InstLemma  `quotient-dep-function-subtype`  []
  THEN  (ParallelLast'  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto)
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x.A\mkleeneclose{};\mkleeneopen{}\mlambda{}x,a,b.  E[a;b]\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  All  (RepUR  ``so\_apply``)
  THEN  Auto)

---

Home Index