---

Step * of Lemma csm-id-adjoin-ap

∀X:CubicalSet. ∀A:{X ⊢ _}. ∀u:{X ⊢ _:A}. ∀I:Cname List. ∀a:X(I).  (([u])a = (a;u I a) ∈ X.A(I))
BY
{ (Auto
   THEN DVar `u'
   THEN (RepUR ``csm-id-adjoin csm-adjoin csm-ap csm-id identity-trans cat-id`` 0 THEN RepUR ``type-cat`` 0)
   THEN Fold `cc-adjoin-cube` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}X:CubicalSet.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}u:\{X  \mvdash{}  \_:A\}.  \mforall{}I:Cname  List.  \mforall{}a:X(I).    (([u])a  =  (a;u  I  a))


By

---

Latex:
(Auto
  THEN  DVar  `u'
  THEN  (RepUR  ``csm-id-adjoin  csm-adjoin  csm-ap  csm-id  identity-trans  cat-id``  0
              THEN  RepUR  ``type-cat``  0
              )
  THEN  Fold  `cc-adjoin-cube`  0
  THEN  Auto)

---

Home Index