---

Step * of Lemma csm-m_wf

No Annotations
∀[Gamma:j⊢]. (m ∈ Gamma.𝕀.𝕀 j⟶ Gamma.𝕀)
BY
{ (Intros
   THEN (MemTypeCD THENW MoveToConcl (-1))
   THEN All (RepUR ``op-cat names-cat type-cat cat-ob cat-arrow cat-comp``)
   THEN RepUR ``functor-ob cube-context-adjoin functor-arrow csm-m compose`` 0
   THEN (RWO  "interval-type-at" 0 THENA Auto)
   THEN RepUR ``interval-presheaf cc-adjoin-cube cubical-type-ap-morph interval-type constant-cubical-type`` 0
   THEN Intros
   THEN Repeat (((FunExt THENW Auto) ORELSE (D 0 THENL [Auto; Id])))
   THEN Try (DProdsAndUnions)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  (m  \mmember{}  Gamma.\mBbbI{}.\mBbbI{}  j{}\mrightarrow{}  Gamma.\mBbbI{})


By

---

Latex:
(Intros
  THEN  (MemTypeCD  THENW  MoveToConcl  (-1))
  THEN  All  (RepUR  ``op-cat  names-cat  type-cat  cat-ob  cat-arrow  cat-comp``)
  THEN  RepUR  ``functor-ob  cube-context-adjoin  functor-arrow  csm-m  compose``  0
  THEN  (RWO    "interval-type-at"  0  THENA  Auto)
  THEN  ...
  THEN  Intros
  THEN  Repeat  (((FunExt  THENW  Auto)  ORELSE  (D  0  THENL  [Auto;  Id])))
  THEN  Try  (DProdsAndUnions)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index