---

Step * 2 2 of Lemma cubical-pi_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. ∀I:Cname List. ∀a:X(I). ∀u:cubical-pi-family(X;A;B;I;a).  ((λK,g. (u K (1 o g))) = u ∈ cubical-pi-family(X;A;B;I;a))
5. I : Cname List
6. J : Cname List
7. K : Cname List
8. f : name-morph(I;J)
9. g : name-morph(J;K)
10. a : X(I)
11. u : cubical-pi-family(X;A;B;I;a)
⊢ (λK,g@0. (u K ((f o g) o g@0))) = (λK,g@0. (u K (f o (g o g@0)))) ∈ cubical-pi-family(X;A;B;K;(f o g)(a))
BY
{ (All Thin THEN D -1 THEN EqTypeCD THEN Reduce 0 THEN Auto) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : Cname List
5. J : Cname List
6. K : Cname List
7. f : name-morph(I;J)
8. g : name-morph(J;K)
9. a : X(I)
10. u : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))
11. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u@0:A(f(a)).
      ((u J f u@0 (f(a);u@0) g) = (u K (f o g) (u@0 f(a) g)) ∈ B(g((f(a);u@0))))
12. J1 : Cname List
13. K@0 : Cname List
14. f@0 : name-morph(K;J1)
15. g@0 : name-morph(J1;K@0)
16. u@0 : A(f@0((f o g)(a)))
⊢ (u J1 ((f o g) o f@0) u@0 (f@0((f o g)(a));u@0) g@0)
= (u K@0 ((f o g) o (f@0 o g@0)) (u@0 f@0((f o g)(a)) g@0))
∈ B(g@0((f@0((f o g)(a));u@0)))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  \mforall{}I:Cname  List.  \mforall{}a:X(I).  \mforall{}u:cubical-pi-family(X;A;B;I;a).    ((\mlambda{}K,g.  (u  K  (1  o  g)))  =  u)
5.  I  :  Cname  List
6.  J  :  Cname  List
7.  K  :  Cname  List
8.  f  :  name-morph(I;J)
9.  g  :  name-morph(J;K)
10.  a  :  X(I)
11.  u  :  cubical-pi-family(X;A;B;I;a)
\mvdash{}  (\mlambda{}K,g@0.  (u  K  ((f  o  g)  o  g@0)))  =  (\mlambda{}K,g@0.  (u  K  (f  o  (g  o  g@0))))


By

---

Latex:
(All  Thin  THEN  D  -1  THEN  EqTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index