---

Step * 1 1 2 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)) s) = (X2 K K-[f j] (f j:=c) (X2 I K f s)) ∈ (X1 K-[f j])
⊢ (X2 I-[j] K-[f j] f (X2 I I-[j] (j:=c) s)) = (X2 I K-[f j] (f o (f j:=c)) s) ∈ (X1 K-[f j])
BY
{ TACTIC:(InstHyp [⌜I⌝; ⌜I-[j]⌝;⌜K-[f j]⌝;⌜(j:=c)⌝;⌜f⌝] 3⋅ THENA Auto) }

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

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


By

---

Latex:
TACTIC:(InstHyp  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}I-[j]\mkleeneclose{};\mkleeneopen{}K-[f  j]\mkleeneclose{};\mkleeneopen{}(j:=c)\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  3\mcdot{}  THENA  Auto)

---

Home Index