---

Step * 1 of Lemma cube-set-map-subtype


1. A : CubicalSet
2. B : CubicalSet
3. x : A@0:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (A A@0) (B A@0))
⊢ x ∈ I:(Cname List) ⟶ A(I) ⟶ B(I)
BY
{ xxx((Fold `I-cube` (-1) THEN RepUR ``cat-arrow type-cat cat-ob name-cat`` -1) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  A  :  CubicalSet
2.  B  :  CubicalSet
3.  x  :  A@0:cat-ob(NameCat)  {}\mrightarrow{}  (cat-arrow(TypeCat)  (A  A@0)  (B  A@0))
\mvdash{}  x  \mmember{}  I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)


By

---

Latex:
xxx((Fold  `I-cube`  (-1)  THEN  RepUR  ``cat-arrow  type-cat  cat-ob  name-cat``  -1)  THEN  Auto)xxx

---

Home Index