---

Step * 1 1 of Lemma discrete-fun-app-invariant


1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. I : fset(ℕ)
5. a : ()(I)
6. (f I a) = (f {} ⋅) ∈ (discr(A) ⟶ discr(B))(a)
7. t : A
⊢ (f I a I 1 t) = (f {} ⋅ {} 1 t) ∈ B
BY
{ RepUR ``cubical-fun cubical-fun-family discrete-cubical-type`` -2 }

1
1. A : Type
2. B : Type
3. f : {() ⊢ _:(discr(A) ⟶ discr(B))}
4. I : fset(ℕ)
5. a : ()(I)
6. (f I a)
= (f {} ⋅)
∈ {w:J:fset(ℕ) ⟶ f:J ⟶ I ⟶ u:A ⟶ B| ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A.  ((w J f u) = (w K f ⋅ g u) ∈ B)} 
7. t : A
⊢ (f I a I 1 t) = (f {} ⋅ {} 1 t) ∈ B

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  \{()  \mvdash{}  \_:(discr(A)  {}\mrightarrow{}  discr(B))\}
4.  I  :  fset(\mBbbN{})
5.  a  :  ()(I)
6.  (f  I  a)  =  (f  \{\}  \mcdot{})
7.  t  :  A
\mvdash{}  (f  I  a  I  1  t)  =  (f  \{\}  \mcdot{}  \{\}  1  t)


By

---

Latex:
RepUR  ``cubical-fun  cubical-fun-family  discrete-cubical-type``  -2

---

Home Index