---

Step * of Lemma all-quotient

∀T:Type
  (canonicalizable(T)
  ⇒ (∀S:Type. ∀E:S ⟶ S ⟶ ℙ.
        (EquivRel(S;a,b.E[a;b]) ⇒ (∀t:T. (x,y:S//E[x;y]) ⇐⇒ f,g:∀t:T. S//fun-equiv(T;a,b.↓E[a;b];f;g)))))
BY
{ (InstLemma `all-quotient-dependent` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜λt.S⌝  THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜λt.E⌝  THENA Auto)
   THEN All (RepUR ``so_apply``)
   THEN (Trivial ⋅ ORELSE ((ParallelLast' THENA Auto) THEN D -1 THEN D 0 THEN (D 0 THENA EAuto 2) THEN Auto))) }

1
1. T : Type
2. canonicalizable(T)
3. S : Type
4. E : S ⟶ S ⟶ ℙ
5. EquivRel(S;a,b.E a b)
6. (∀t:T. (x,y:S//(E x y))) ⇒ (f,g:∀t:T. S//dep-fun-equiv(T;t,x,y.↓E x y;f;g))
7. (∀t:T. (x,y:S//(E x y))) ⇐ f,g:∀t:T. S//dep-fun-equiv(T;t,x,y.↓E x y;f;g)
8. f,g:∀t:T. S//fun-equiv(T;a,b.↓E a b;f;g)
9. t : T
⊢ x,y:S//(E x y)

---

Latex:

---

Latex:
\mforall{}T:Type
    (canonicalizable(T)
    {}\mRightarrow{}  (\mforall{}S:Type.  \mforall{}E:S  {}\mrightarrow{}  S  {}\mrightarrow{}  \mBbbP{}.
                (EquivRel(S;a,b.E[a;b])
                {}\mRightarrow{}  (\mforall{}t:T.  (x,y:S//E[x;y])  \mLeftarrow{}{}\mRightarrow{}  f,g:\mforall{}t:T.  S//fun-equiv(T;a,b.\mdownarrow{}E[a;b];f;g)))))


By

---

Latex:
(InstLemma  `all-quotient-dependent`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}t.S\mkleeneclose{}    THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}t.E\mkleeneclose{}    THENA  Auto)
  THEN  All  (RepUR  ``so\_apply``)
  THEN  (Trivial
              \mcdot{}
  ORELSE  ((ParallelLast'  THENA  Auto)  THEN  D  -1  THEN  D  0  THEN  (D  0  THENA  EAuto  2)  THEN  Auto)
  ))

---

Home Index