---

Step * of Lemma refl-map_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}].  (refl-map(X;A) ∈ {X ⊢ _:(A ⟶ discr({X.A ⊢ _:Path((A)p)}))})
BY
{ (Intros
   THEN (Assert refl(q) ∈ {X.A ⊢ _:Path((A)p)} BY
               (SubsumeC ⌜{X.A ⊢ _:(Path_(A)p q q)}⌝⋅ THEN Auto))
   THEN (Assert discr(refl(q)) ∈ {X.A ⊢ _:(discr({X.A ⊢ _:Path((A)p)}))p} BY
               (RWO "csm-discrete-cubical-type" 0 THEN Auto))
   THEN Unfold `refl-map` 0
   THEN (InstLemma `cubical-lam_wf` [⌜parm{j}⌝;⌜parm{[i | j]'}⌝]⋅ THEN BHyp -1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    (refl-map(X;A)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  discr(\{X.A  \mvdash{}  \_:Path((A)p)\}))\})


By

---

Latex:
(Intros
  THEN  (Assert  refl(q)  \mmember{}  \{X.A  \mvdash{}  \_:Path((A)p)\}  BY
                          (SubsumeC  \mkleeneopen{}\{X.A  \mvdash{}  \_:(Path\_(A)p  q  q)\}\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  discr(refl(q))  \mmember{}  \{X.A  \mvdash{}  \_:(discr(\{X.A  \mvdash{}  \_:Path((A)p)\}))p\}  BY
                          (RWO  "csm-discrete-cubical-type"  0  THEN  Auto))
  THEN  Unfold  `refl-map`  0
  THEN  (InstLemma  `cubical-lam\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{[i  |  j]'\}\mkleeneclose{}]\mcdot{}  THEN  BHyp  -1)
  THEN  Auto)

---

Home Index