---

Step * 1 2 2 2 of Lemma csm-cubical-pi-family


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)) = (λx.(X2 J K g (X2 I J f x))) ∈ ((X1 I) ⟶ (X1 K)))
4. ∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I)))
5. X : L:(Cname List) ⟶ Type
6. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
7. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((D1 I K (f o g)) = (λx.(D1 J K g (D1 I J f x))) ∈ ((X I) ⟶ (X K)))
8. ∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))
9. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type
10. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X1 I) ⟶ (A1 I a) ⟶ (A1 J f(a))
11. ∀I:Cname List. ∀a:X1 I. ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a))
12. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X1 I. ∀u:A1 I a.
      ((A2 I K (f o g) a u) = (A2 J K g f(a) (A2 I J f a u)) ∈ (A1 K (f o g)(a)))
13. A : I:(Cname List) ⟶ (alpha:X1 I × (A1 I alpha)) ⟶ Type
14. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(alpha:X1 I × (A1 I alpha)) ⟶ (A I a) ⟶ (A J f(a))
15. ∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a.  ((B1 I I 1 a u) = u ∈ (A I a))
16. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a.
      ((B1 I K (f o g) a u) = (B1 J K g f(a) (B1 I J f a u)) ∈ (A K (f o g)(a)))
17. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)
18. ∀A,B:Cname List. ∀g:name-morph(A;B).  ((λx.(X2 A B g (s A x))) = (λx.(s B (D1 A B g x))) ∈ ((X A) ⟶ (X1 B)))
19. I : Cname List
20. a : X I
21. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J f(s I a)) ⟶ (A J <f(s I a), u>)
22. J : Cname List
23. K : Cname List
24. f : name-morph(I;J)
25. g : name-morph(J;K)
26. u : A1 J f(s I a)
27. f(s I a) = (s J f(a)) ∈ (X1 J)
28. (X2 I J f (s I a)) = (s J (D1 I J f a)) ∈ (X1 J)
⊢ (A2 J K g (X2 I J f (s I a)) u) = (A2 J K g (s J (D1 I J f a)) u) ∈ (A1 K (X2 J K g (X2 I J f (s I a))))
BY
{ TACTIC:(Subst ⌜(s J (D1 I J f a)) = (X2 I J f (s I a)) ∈ {z:X1 J| z = (X2 I J f (s I a)) ∈ (X1 J)} ⌝ 0⋅
          THEN All (RepUR ``cube-set-restriction``)
          THEN Auto) }

---

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))  =  (\mlambda{}x.(X2  J  K  g  (X2  I  J  f  x))))
4.  \mforall{}I:Cname  List.  ((X2  I  I  1)  =  (\mlambda{}x.x))
5.  X  :  L:(Cname  List)  {}\mrightarrow{}  Type
6.  D1  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J)
7.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
          ((D1  I  K  (f  o  g))  =  (\mlambda{}x.(D1  J  K  g  (D1  I  J  f  x))))
8.  \mforall{}I:Cname  List.  ((D1  I  I  1)  =  (\mlambda{}x.x))
9.  A1  :  I:(Cname  List)  {}\mrightarrow{}  (X1  I)  {}\mrightarrow{}  Type
10.  A2  :  I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  f:name-morph(I;J)
{}\mrightarrow{}  a:(X1  I)
{}\mrightarrow{}  (A1  I  a)
{}\mrightarrow{}  (A1  J  f(a))
11.  \mforall{}I:Cname  List.  \mforall{}a:X1  I.  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u)
12.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:X1  I.  \mforall{}u:A1  I  a.
            ((A2  I  K  (f  o  g)  a  u)  =  (A2  J  K  g  f(a)  (A2  I  J  f  a  u)))
13.  A  :  I:(Cname  List)  {}\mrightarrow{}  (alpha:X1  I  \mtimes{}  (A1  I  alpha))  {}\mrightarrow{}  Type
14.  B1  :  I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  f:name-morph(I;J)
{}\mrightarrow{}  a:(alpha:X1  I  \mtimes{}  (A1  I  alpha))
{}\mrightarrow{}  (A  I  a)
{}\mrightarrow{}  (A  J  f(a))
15.  \mforall{}I:Cname  List.  \mforall{}a:alpha:X1  I  \mtimes{}  (A1  I  alpha).  \mforall{}u:A  I  a.    ((B1  I  I  1  a  u)  =  u)
16.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).  \mforall{}a:alpha:X1  I  \mtimes{}  (A1  I  alpha).  \mforall{}u:A  I 
                                                                                                                                                                                                a.
            ((B1  I  K  (f  o  g)  a  u)  =  (B1  J  K  g  f(a)  (B1  I  J  f  a  u)))
17.  s  :  A:(Cname  List)  {}\mrightarrow{}  (X  A)  {}\mrightarrow{}  (X1  A)
18.  \mforall{}A,B:Cname  List.  \mforall{}g:name-morph(A;B).    ((\mlambda{}x.(X2  A  B  g  (s  A  x)))  =  (\mlambda{}x.(s  B  (D1  A  B  g  x))))
19.  I  :  Cname  List
20.  a  :  X  I
21.  w  :  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  u:(A1  J  f(s  I  a))  {}\mrightarrow{}  (A  J  <f(s  I  a),  u>)
22.  J  :  Cname  List
23.  K  :  Cname  List
24.  f  :  name-morph(I;J)
25.  g  :  name-morph(J;K)
26.  u  :  A1  J  f(s  I  a)
27.  f(s  I  a)  =  (s  J  f(a))
28.  (X2  I  J  f  (s  I  a))  =  (s  J  (D1  I  J  f  a))
\mvdash{}  (A2  J  K  g  (X2  I  J  f  (s  I  a))  u)  =  (A2  J  K  g  (s  J  (D1  I  J  f  a))  u)


By

---

Latex:
TACTIC:(Subst  \mkleeneopen{}(s  J  (D1  I  J  f  a))  =  (X2  I  J  f  (s  I  a))\mkleeneclose{}  0\mcdot{}
                THEN  All  (RepUR  ``cube-set-restriction``)
                THEN  Auto)

---

Home Index