---

Step * of Lemma respects-equality-function

∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
  ((A' ⊆r A) ⇒ (∀a:A'. respects-equality(B[a];B'[a])) ⇒ respects-equality(a:A ⟶ B[a];a:A' ⟶ B'[a]))
BY
{ (Auto THEN RepeatFor 4 ((D 0 THENW Auto)) THEN (FunExt THENA Auto)) }

1
1. A : Type
2. A' : Type
3. B : A ⟶ Type
4. B' : A' ⟶ Type
5. A' ⊆r A
6. ∀a:A'. respects-equality(B[a];B'[a])
7. x : Base
8. y : Base
9. x = y ∈ (a:A ⟶ B[a])
10. x ∈ a:A' ⟶ B'[a]
11. a : A'
⊢ (x a) = (y a) ∈ B'[a]

---

Latex:

---

Latex:
\mforall{}[A,A':Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[B':A'  {}\mrightarrow{}  Type].
    ((A'  \msubseteq{}r  A)
    {}\mRightarrow{}  (\mforall{}a:A'.  respects-equality(B[a];B'[a]))
    {}\mRightarrow{}  respects-equality(a:A  {}\mrightarrow{}  B[a];a:A'  {}\mrightarrow{}  B'[a]))


By

---

Latex:
(Auto  THEN  RepeatFor  4  ((D  0  THENW  Auto))  THEN  (FunExt  THENA  Auto))

---

Home Index