---

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

.....wf..... 
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 ∈ name-morph(I-[j];K-[f j])
BY
{ TACTIC:(Assert j ∈ {x:nameset(I)| ↑isname(f x)}  BY
                (DoSubsume THEN Auto)) }

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])
13. j = j ∈ name-morph-domain(f;I)
⊢ name-morph-domain(f;I) ⊆r {x:nameset(I)| ↑isname(f x)} 

2
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])
13. j ∈ {x:nameset(I)| ↑isname(f x)} 
⊢ f ∈ name-morph(I-[j];K-[f j])

---

Latex:

---

Latex:
.....wf..... 
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  \mmember{}  name-morph(I-[j];K-[f  j])


By

---

Latex:
TACTIC:(Assert  j  \mmember{}  \{x:nameset(I)|  \muparrow{}isname(f  x)\}    BY
                            (DoSubsume  THEN  Auto))

---

Home Index