---

Step * 1 of Lemma function-eq-symmetry-type-function


1. A : Type@i'
2. B : type-function{i:l}(A)@i'
3. f : Base@i
4. g : Base@i
⊢ function-eq(A;a.B[a];f;g) ⇒ function-eq(A;a.B[a];g;f)
BY
{ PointwiseFunctionality 2 }

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
⊢ function-eq(A;a@0.a[a@0];f;g) ⇒ function-eq(A;a@0.a[a@0];g;f)

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
⊢ (function-eq(A;a@0.a[a@0];f;g) ⇒ function-eq(A;a@0.a[a@0];g;f))
= (function-eq(A;a.b[a];f;g) ⇒ function-eq(A;a.b[a];g;f))
∈ Type

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  B  :  type-function\{i:l\}(A)@i'
3.  f  :  Base@i
4.  g  :  Base@i
\mvdash{}  function-eq(A;a.B[a];f;g)  {}\mRightarrow{}  function-eq(A;a.B[a];g;f)


By

---

Latex:
PointwiseFunctionality  2

---

Home Index