---

Step * 2 2 of Lemma cubical-lambda_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : {X.A ⊢ _:B}
5. I : Cname List
6. J : Cname List
7. f : name-morph(I;J)
8. a : X(I)
9. J@0 : Cname List
10. K : Cname List
11. f@0 : name-morph(J;J@0)
12. g : name-morph(J@0;K)
13. u : A(f@0(f(a)))
⊢ (b J@0 ((f o f@0)(a);u) (f@0(f(a));u) g) = (b K ((f o (f@0 o g))(a);(u f@0(f(a)) g))) ∈ B(g((f@0(f(a));u)))
BY
{ ((RenameVar `H' (-5) THEN RenameVar `h' (-3))
   THEN (RepeatFor 2 (DVar `B') THEN DVar `b')
   THEN All Reduce
   THEN RepUR ``cubical-type-ap-morph cubical-type-at`` 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((RenameVar  `H'  (-5)  THEN  RenameVar  `h'  (-3))
  THEN  (RepeatFor  2  (DVar  `B')  THEN  DVar  `b')
  THEN  All  Reduce
  THEN  RepUR  ``cubical-type-ap-morph  cubical-type-at``  0)

---

Home Index