---

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


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])
BY
{ TACTIC:((ApFunToHypEquands `Z' ⌜Z s⌝ ⌜X1 K-[f j]⌝ (-1)⋅ THENA Auto) THEN RepUR ``compose`` -1 THEN Thin (-2)) }

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)) s) = (X2 K K-[f j] (f j:=c) (X2 I K f s)) ∈ (X1 K-[f j])
⊢ (f j:=c)(f(s)) = f((j:=c)(s)) ∈ <X1, X2>(K-[f j])

---

Latex:

---

Latex:

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)))  =  ((X2  K  K-[f  j]  (f  j:=c))  o  (X2  I  K  f))
\mvdash{}  (f  j:=c)(f(s))  =  f((j:=c)(s))


By

---

Latex:
TACTIC:((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  s\mkleeneclose{}  \mkleeneopen{}X1  K-[f  j]\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                THEN  RepUR  ``compose``  -1
                THEN  Thin  (-2))

---

Home Index