---

Step * 3 of Lemma csm-cubical-isect

.....eq aux..... 
1. X : CubicalSet
2. Delta : CubicalSet
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. s : Delta ⟶ X
6. A1 : I:fset(ℕ) ⟶ Delta(I) ⟶ Type
⊢ (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Delta(I) ⟶ (A1 I a) ⟶ (A1 J f(a)))
= (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Delta(I) ⟶ (A1 I a) ⟶ (A1 J f(a)))
∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  X  :  CubicalSet
2.  Delta  :  CubicalSet
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  s  :  Delta  {}\mrightarrow{}  X
6.  A1  :  I:fset(\mBbbN{})  {}\mrightarrow{}  Delta(I)  {}\mrightarrow{}  Type
\mvdash{}  (I:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  a:Delta(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a)))
=  (I:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  a:Delta(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a)))


By

---

Latex:
Auto

---

Home Index