---

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

.....subterm..... T:t
3:n
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)) s) = (X2 K K-[f j] (f j:=c) (X2 I K f s)) ∈ (X1 K-[f j])
⊢ (f j:=c)(f(s)) = (X2 K K-[f j] (f j:=c) (X2 I K f s)) ∈ <X1, X2>(K-[f j])
BY
{ TACTIC:(RepUR ``cube-set-restriction I-cube`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  X1  :  L:(Cname  List)  {}\mrightarrow{}  Type
2.  X2  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X1  I)  {}\mrightarrow{}  (X1  J)
3.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
          ((X2  I  K  (f  o  g))  =  ((X2  J  K  g)  o  (X2  I  J  f)))
4.  \mforall{}I:Cname  List.  ((X2  I  I  1)  =  (\mlambda{}x.x))
5.  I  :  Cname  List
6.  K  :  Cname  List
7.  f  :  name-morph(I;K)
8.  s  :  X1  I
9.  c  :  \mBbbN{}2
10.  j  :  name-morph-domain(f;I)
11.  f  j  \mmember{}  nameset(K)
12.  (X2  I  K-[f  j]  (f  o  (f  j:=c))  s)  =  (X2  K  K-[f  j]  (f  j:=c)  (X2  I  K  f  s))
\mvdash{}  (f  j:=c)(f(s))  =  (X2  K  K-[f  j]  (f  j:=c)  (X2  I  K  f  s))


By

---

Latex:
TACTIC:(RepUR  ``cube-set-restriction  I-cube``  0  THEN  Auto)

---

Home Index