---

Step * 1 of Lemma csm-path-type

.....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)))
BY
{ (BLemma `cubical-type-restriction-and`
   THENA (Auto THEN Try (OnVar `t' (RepUR ``pathtype cubical-fun cubical-fun-family csm-ap-type``)) THEN Auto)
   ) }

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

2
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 1) = b((s)a1) ∈ A((s)a1))

---

Latex:

---

Latex:
.....antecedent..... 
1.  X  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  s  :  Delta  j{}\mrightarrow{}  X
4.  A  :  \{X  \mvdash{}  \_\}
5.  a  :  \{X  \mvdash{}  \_:A\}
6.  b  :  \{X  \mvdash{}  \_:A\}
\mvdash{}  cubical-type-restriction(Delta;(Path(A))s;I,a1,t.((t  I  1  0)  =  a((s)a1))  \mwedge{}  ((t  I  1  1)  =  b((s)a1)))


By

---

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

---

Home Index