---

Step * of Lemma cubical-pi-family-comp

∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.
∀w:cubical-pi-family(X;A;B;I;(s)a).
  (λK,g. (w K (f o g)) ∈ cubical-pi-family(X;A;B;J;(s)f(a)))
BY
{ (Auto
   THEN D -1
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``cubical-type-ap-morph`` 0
   THEN RenameVar `H' (-5)
   THEN RenameVar `h' (-3)
   THEN (Assert X ⊢ A ∧ X.A ⊢ B BY
               Auto)
   THEN RepeatFor 2 (DVar `A')
   THEN RepeatFor 2 (DVar `B')
   THEN All Reduce) }

1
1. X : CubicalSet
2. Delta : CubicalSet
3. s : Delta ⟶ X
4. I : Cname List
5. J : Cname List
6. f : name-morph(I;J)
7. a : Delta(I)
8. A1 : I:(Cname List) ⟶ X(I) ⟶ Type
9. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
10. (∀I:Cname List. ∀a:X(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:X(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))))
11. A : I:(Cname List) ⟶ X.<A1, A2>(I) ⟶ Type
12. B1 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:X.<A1, A2>(I) ⟶ (A I a) ⟶ (A J f(a))
13. (∀I:Cname List. ∀a:X.<A1, A2>(I). ∀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:X.<A1, A2>(I). ∀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))))
14. w : J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:<A1, A2>(f((s)a)) ⟶ <A, B1>((f((s)a);u))
15. ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:<A1, A2>(f((s)a)).
      ((w J f u (f((s)a);u) g) = (w K (f o g) (u f((s)a) g)) ∈ <A, B1>(g((f((s)a);u))))
16. H : Cname List
17. K : Cname List
18. h : name-morph(J;H)
19. g : name-morph(H;K)
20. u : <A1, A2>(h((s)f(a)))
21. X ⊢ <A1, A2> ∧ X.<A1, A2> ⊢ <A, B1>
⊢ (B1 H K g ((s)h(f(a));u) (w H (f o h) u)) = (w K (f o (h o g)) (A2 H K g (s)h(f(a)) u)) ∈ <A, B1>(g(((s)h(f(a));u)))

---

Latex:

---

Latex:
\mforall{}X,Delta:CubicalSet.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:Delta(I).  \mforall{}A:\{X  \mvdash{}  \_\}.
\mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}w:cubical-pi-family(X;A;B;I;(s)a).
    (\mlambda{}K,g.  (w  K  (f  o  g))  \mmember{}  cubical-pi-family(X;A;B;J;(s)f(a)))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``cubical-type-ap-morph``  0
  THEN  RenameVar  `H'  (-5)
  THEN  RenameVar  `h'  (-3)
  THEN  (Assert  X  \mvdash{}  A  \mwedge{}  X.A  \mvdash{}  B  BY
                          Auto)
  THEN  RepeatFor  2  (DVar  `A')
  THEN  RepeatFor  2  (DVar  `B')
  THEN  All  Reduce)

---

Home Index