---

Step * 1 of Lemma discrete-fun_wf


1. A : Type
2. B : Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:(discr(A) ⟶ discr(B))}
⊢ λI,alpha. (f I alpha I 1) ∈ {X ⊢ _:discr(A ⟶ B)}
BY
{ MemTypeCD }

1
1. A : Type
2. B : Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:(discr(A) ⟶ discr(B))}
⊢ λI,alpha. (f I alpha I 1) ∈ I:fset(ℕ) ⟶ a:X(I) ⟶ discr(A ⟶ B)(a)

2
.....set predicate..... 
1. A : Type
2. B : Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:(discr(A) ⟶ discr(B))}
⊢ ∀I,J:fset(ℕ). ∀f@0:J ⟶ I. ∀a:X(I).
    (((λI,alpha. (f I alpha I 1)) I a a f@0) = ((λI,alpha. (f I alpha I 1)) J f@0(a)) ∈ discr(A ⟶ B)(f@0(a)))

3
.....wf..... 
1. A : Type
2. B : Type
3. X : CubicalSet{j}
4. f : {X ⊢ _:(discr(A) ⟶ discr(B))}
5. u : I:fset(ℕ) ⟶ a:X(I) ⟶ discr(A ⟶ B)(a)
⊢ istype(∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((u I a a f) = (u J f(a)) ∈ discr(A ⟶ B)(f(a))))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  X  :  CubicalSet\{j\}
4.  f  :  \{X  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
\mvdash{}  \mlambda{}I,alpha.  (f  I  alpha  I  1)  \mmember{}  \{X  \mvdash{}  \_:discr(A  {}\mrightarrow{}  B)\}


By

---

Latex:
MemTypeCD

---

Home Index