---

Step * of Lemma cube-set-restriction-face-map

∀[X:CubicalSet]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[s:X(I)]. ∀[c:ℕ2]. ∀[j:name-morph-domain(f;I)].
  ((f j:=c)(f(s)) = f((j:=c)(s)) ∈ X(K-[f j]))
BY
{ TACTIC:((Auto THEN (Assert f j ∈ nameset(K) BY (InstLemma `name-morph_subtype_domain` [⌜I⌝;⌜K⌝;⌜f⌝]⋅ THEN Auto)))
          THEN RepeatFor 2 (D 1)
          THEN All Reduce
          THEN D 3
          THEN (InstHyp [⌜I⌝; ⌜K⌝;⌜K-[f j]⌝;⌜f⌝;⌜(f j:=c)⌝] 3⋅ THENA Auto)
          THEN RepUR ``I-cube functor-ob`` -5) }

1
1. X1 : L:(Cname List) ⟶ Type
2. X2 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X1 I) ⟶ (X1 J)
3. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((X2 I K (f o g)) = ((X2 J K g) o (X2 I J f)) ∈ ((X1 I) ⟶ (X1 K)))
4. ∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I)))
5. I : Cname List
6. K : Cname List
7. f : name-morph(I;K)
8. s : X1 I
9. c : ℕ2
10. j : name-morph-domain(f;I)
11. f j ∈ nameset(K)
12. (X2 I K-[f j] (f o (f j:=c))) = ((X2 K K-[f j] (f j:=c)) o (X2 I K f)) ∈ ((X1 I) ⟶ (X1 K-[f j]))
⊢ (f j:=c)(f(s)) = f((j:=c)(s)) ∈ <X1, X2>(K-[f j])

---

Latex:

---

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,K:Cname  List].  \mforall{}[f:name-morph(I;K)].  \mforall{}[s:X(I)].  \mforall{}[c:\mBbbN{}2].
\mforall{}[j:name-morph-domain(f;I)].
    ((f  j:=c)(f(s))  =  f((j:=c)(s)))


By

---

Latex:
TACTIC:((Auto
                  THEN  (Assert  f  j  \mmember{}  nameset(K)  BY
                                          (InstLemma  `name-morph\_subtype\_domain`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto))
                  )
                THEN  RepeatFor  2  (D  1)
                THEN  All  Reduce
                THEN  D  3
                THEN  (InstHyp  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}K-[f  j]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}(f  j:=c)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
                THEN  RepUR  ``I-cube  functor-ob``  -5)

---

Home Index