---

Step * 1 2 of Lemma path-restriction


1. [X] : CubicalSet{j}
2. [A] : {X ⊢ _}
3. [a] : {X ⊢ _:A}
4. [b] : {X ⊢ _:A}
⊢ cubical-type-restriction(X;Path(A);I,a1,p.(p I 1 1) = b(a1) ∈ A(a1))
BY
{ (InstLemma `cubical-type-restriction-eq` [⌜X⌝;⌜Path(A)⌝;⌜A⌝;⌜b⌝;⌜so_lambda(I,alpha,p.p I 1 1)⌝]⋅
   THEN Auto
   THEN Try ((OnVar `p' (RepUR ``pathtype cubical-fun cubical-fun-family``) THEN Auto))) }

1
1. X : CubicalSet{j}
2. A : {X ⊢ _}
3. a : {X ⊢ _:A}
4. b : {X ⊢ _:A}
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. alpha : X(I)
9. t : Path(A)(alpha)
⊢ ((t alpha f) J 1 1) = (t I 1 1 alpha f) ∈ A(f(alpha))

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet\{j\}
2.  [A]  :  \{X  \mvdash{}  \_\}
3.  [a]  :  \{X  \mvdash{}  \_:A\}
4.  [b]  :  \{X  \mvdash{}  \_:A\}
\mvdash{}  cubical-type-restriction(X;Path(A);I,a1,p.(p  I  1  1)  =  b(a1))


By

---

Latex:
(InstLemma  `cubical-type-restriction-eq`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Path(A)\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}so\_lambda(I,alpha,p.p  I  1  1)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)))

---

Home Index