---

Step * of Lemma cube-set-map-is

∀[A,B:CubicalSet].
  (A ⟶ B ~ {trans:I:(Cname List) ⟶ A(I) ⟶ B(I)| 
             ∀I,J:Cname List. ∀g:name-morph(I;J).  ((λs.g(trans I s)) = (λs.(trans J g(s))) ∈ (A(I) ⟶ B(J)))} )
BY
{ (Auto
   THEN RepUR ``I-cube cube-set-restriction cube-set-map name-cat type-cat nat-trans `` 0
   THEN RepUR ``cat-comp functor-arrow cat-ob cat-arrow compose`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:CubicalSet].
    (A  {}\mrightarrow{}  B  \msim{}  \{trans:I:(Cname  List)  {}\mrightarrow{}  A(I)  {}\mrightarrow{}  B(I)| 
                          \mforall{}I,J:Cname  List.  \mforall{}g:name-morph(I;J).    ((\mlambda{}s.g(trans  I  s))  =  (\mlambda{}s.(trans  J  g(s))))\}  )


By

---

Latex:
(Auto
  THEN  RepUR  ``I-cube  cube-set-restriction  cube-set-map  name-cat  type-cat  nat-trans  ``  0
  THEN  RepUR  ``cat-comp  functor-arrow  cat-ob  cat-arrow  compose``  0
  THEN  Auto)

---

Home Index