---

Step * of Lemma all-quotient-dependent

∀T:Type
  (canonicalizable(T)
  ⇒ (∀S:T ⟶ ℙ. ∀E:t:T ⟶ S[t] ⟶ S[t] ⟶ ℙ.
        ((∀t:T. EquivRel(S t;a,b.E[t;a;b]))
        ⇒ (∀t:T. (x,y:S[t]//E[t;x;y]) ⇐⇒ f,g:∀t:T. S[t]//dep-fun-equiv(T;t,x,y.↓E[t;x;y];f;g)))))
BY
{ (RepUR ``so_apply`` 0 THEN Auto THEN Try ((BLemma `dep-fun-equiv-rel` THEN EAuto 2))) }

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

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

---

Latex:

---

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


By

---

Latex:
(RepUR  ``so\_apply``  0  THEN  Auto  THEN  Try  ((BLemma  `dep-fun-equiv-rel`  THEN  EAuto  2)))

---

Home Index