---

Step * of Lemma base-type-family-implies

∀[A:Type]. ∀[B:Base].  ∀a:A. (B[a] ∈ Type) supposing base-type-family{i:l}(A;a.B[a])
BY
{ (Auto THEN PointwiseFunctionality (-1))⋅ }

1
1. A : Type
2. B : Base
3. base-type-family{i:l}(A;a.B[a])
4. [a1] : Base
5. [b] : Base
6. [c] : a1 = b ∈ A
⊢ B[a1] ∈ Type

2
1. A : Type
2. B : Base
3. base-type-family{i:l}(A;a.B[a])
4. a1 : Base
5. b : Base
6. c : a1 = b ∈ A
⊢ (B[a1] ∈ Type) = (B[b] ∈ Type) ∈ 𝕌'

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:Base].    \mforall{}a:A.  (B[a]  \mmember{}  Type)  supposing  base-type-family\{i:l\}(A;a.B[a])


By

---

Latex:
(Auto  THEN  PointwiseFunctionality  (-1))\mcdot{}

---

Home Index