---

Step * of Lemma function-eq-transitivity-type-function

∀A:Type. ∀B:type-function{i:l}(A). ∀f,g,h:Base.
  (function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;h) ⇒ function-eq(A;a.B[a];f;h))
BY
{ (RepeatFor 5 (Intro)
   THEN PointwiseFunctionality 2
   THEN (Assert base-type-family{i:l}(A;x.a[x]) BY
               (D 0 THEN Auto))
   THEN InstLemma `function-eq_wf` [⌜A⌝;⌜a⌝]⋅
   THEN Auto) }

1
1. A : Type@i'
2. a : Base
3. b : Base
4. c : a = b ∈ type-function{i:l}(A)
5. f : Base@i
6. g : Base@i
7. h : Base@i
8. base-type-family{i:l}(A;x.a[x])
9. ∀[f,g:Base].  (function-eq(A;a@0.a[a@0];f;g) ∈ Type)
10. function-eq(A;a@0.a[a@0];f;g)@i
11. function-eq(A;a@0.a[a@0];g;h)@i
⊢ function-eq(A;a@0.a[a@0];f;h)

2
1. A : Type@i'
2. a : Base
3. b : Base
4. c : a = b ∈ type-function{i:l}(A)
5. f : Base@i
6. g : Base@i
7. h : Base@i
8. base-type-family{i:l}(A;x.a[x])
9. ∀[f,g:Base].  (function-eq(A;a@0.a[a@0];f;g) ∈ Type)
⊢ (function-eq(A;a@0.a[a@0];f;g) ⇒ function-eq(A;a@0.a[a@0];g;h) ⇒ function-eq(A;a@0.a[a@0];f;h))
= (function-eq(A;a.b[a];f;g) ⇒ function-eq(A;a.b[a];g;h) ⇒ function-eq(A;a.b[a];f;h))
∈ Type

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:type-function\{i:l\}(A).  \mforall{}f,g,h:Base.
    (function-eq(A;a.B[a];f;g)  {}\mRightarrow{}  function-eq(A;a.B[a];g;h)  {}\mRightarrow{}  function-eq(A;a.B[a];f;h))


By

---

Latex:
(RepeatFor  5  (Intro)
  THEN  PointwiseFunctionality  2
  THEN  (Assert  base-type-family\{i:l\}(A;x.a[x])  BY
                          (D  0  THEN  Auto))
  THEN  InstLemma  `function-eq\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index