---

Step * of Lemma csm-path-type

No Annotations
∀X,Delta:j⊢. ∀s:Delta j⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}.
  (((Path_A a b))s = (Delta ⊢ Path_(A)s (a)s (b)s) ∈ {Delta ⊢ _})
BY
{ (Auto
   THEN RepUR ``path-type`` 0
   THEN (RWO "csm-cubical-subset" 0 THENA Auto)
   THEN EqCD
   THEN Try (OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family csm-ap-type``))
   THEN Auto) }

1
.....antecedent..... 
1. X : CubicalSet{j}
2. Delta : CubicalSet{j}
3. s : Delta j⟶ X
4. A : {X ⊢ _}
5. a : {X ⊢ _:A}
6. b : {X ⊢ _:A}
⊢ cubical-type-restriction(Delta;(Path(A))s;I,a1,t.((t I 1 0) = a((s)a1) ∈ A((s)a1))
∧ ((t I 1 1) = b((s)a1) ∈ A((s)a1)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}X,Delta:j\mvdash{}.  \mforall{}s:Delta  j{}\mrightarrow{}  X.  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}a,b:\{X  \mvdash{}  \_:A\}.
    (((Path\_A  a  b))s  =  (Delta  \mvdash{}  Path\_(A)s  (a)s  (b)s))


By

---

Latex:
(Auto
  THEN  RepUR  ``path-type``  0
  THEN  (RWO  "csm-cubical-subset"  0  THENA  Auto)
  THEN  EqCD
  THEN  Try  (OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family  csm-ap-type``))
  THEN  Auto)

---

Home Index