---

Step * 1 3 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))))
∧ (∀I:Cname List. ((X2 I I 1) = (λx.x) ∈ ((X1 I) ⟶ (X1 I))))
4. X : L:(Cname List) ⟶ Type
5. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
6. (∀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))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
7. A1 : I:(Cname List) ⟶ (X1 I) ⟶ Type
8. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X1 I) ⟶ (A1 I a) ⟶ (A1 J f(a))
9. (∀I:Cname List. ∀a:X1 I. ∀u:A1 I a.  ((A2 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀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))))
10. A : I:(Cname List) ⟶ (alpha:X1 I × (A1 I alpha)) ⟶ Type
11. 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))
12. (∀I:Cname List. ∀a:alpha:X1 I × (A1 I alpha). ∀u:A I a.  ((B1 I I 1 a u) = u ∈ (A I a)))
∧ (∀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))))
13. s : A:(Cname List) ⟶ (X A) ⟶ (X1 A)
14. ∀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)))
15. I : Cname List
16. a : X I
17. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:(A1 J f(s I a)) ⟶ (A J <f(s I a), u>)
18. J : Cname List
19. K : Cname List
20. f : name-morph(I;J)
21. g : name-morph(J;K)
22. u : A1 J f(s I a)
23. alpha : X1 J
24. f(s I a) = (s J f(a)) ∈ (X1 J)
⊢ istype(A1 J alpha)
BY
{ TACTIC:(RepUR ``cube-set-restriction`` 0 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)))))
\mwedge{}  (\mforall{}I:Cname  List.  ((X2  I  I  1)  =  (\mlambda{}x.x)))
4.  X  :  L:(Cname  List)  {}\mrightarrow{}  Type
5.  D1  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J)
6.  (\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)))))
\mwedge{}  (\mforall{}I:Cname  List.  ((D1  I  I  1)  =  (\mlambda{}x.x)))
7.  A1  :  I:(Cname  List)  {}\mrightarrow{}  (X1  I)  {}\mrightarrow{}  Type
8.  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))
9.  (\mforall{}I:Cname  List.  \mforall{}a:X1  I.  \mforall{}u:A1  I  a.    ((A2  I  I  1  a  u)  =  u))
\mwedge{}  (\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))))
10.  A  :  I:(Cname  List)  {}\mrightarrow{}  (alpha:X1  I  \mtimes{}  (A1  I  alpha))  {}\mrightarrow{}  Type
11.  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))
12.  (\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))
\mwedge{}  (\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))))
13.  s  :  A:(Cname  List)  {}\mrightarrow{}  (X  A)  {}\mrightarrow{}  (X1  A)
14.  \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))))
15.  I  :  Cname  List
16.  a  :  X  I
17.  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>)
18.  J  :  Cname  List
19.  K  :  Cname  List
20.  f  :  name-morph(I;J)
21.  g  :  name-morph(J;K)
22.  u  :  A1  J  f(s  I  a)
23.  alpha  :  X1  J
24.  f(s  I  a)  =  (s  J  f(a))
\mvdash{}  istype(A1  J  alpha)


By

---

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

---

Home Index