---

Step * 1 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 0) = a(a1) ∈ A(a1)) ∧ ((p I 1 1) = b(a1) ∈ A(a1)))
BY
{ (BLemma `cubical-type-restriction-and`
   THENA (Auto THEN 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}
⊢ cubical-type-restriction(X;Path(A);I,a1,p.(p I 1 0) = a(a1) ∈ A(a1))

2
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))

---

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  0)  =  a(a1))  \mwedge{}  ((p  I  1  1)  =  b(a1)))


By

---

Latex:
(BLemma  `cubical-type-restriction-and`
  THENA  (Auto  THEN  OnVar  `p'  (RepUR  ``pathtype  cubical-fun  cubical-fun-family``)  THEN  Auto)
  )

---

Home Index