---

Step * 3 1 of Lemma cc-snd_wf


1. X : L:(Cname List) ⟶ Type
2. G1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
3. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
      ((G1 I K (f o g)) = ((G1 J K g) o (G1 I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((G1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
4. A1 : I:(Cname List) ⟶ (X I) ⟶ Type
5. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:(X I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. (∀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))))
7. u : I:(Cname List) ⟶ a:(alpha:X I × (A1 I alpha)) ⟶ ((fst((<A1, A2>)p)) I a)
8. <X, G1> ∈ CubicalSet
⊢ istype(∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:alpha:X I × (A1 I alpha).
           ((A2 I J f (fst(a)) (u I a)) = (u J f(a)) ∈ (A1 J (fst(f(a))))))
BY
{ (RepeatFor 4 (MemCD')
   THEN Try ((Fold `member` 0
              THEN D -1
              THEN RepUR ``cube-set-restriction`` 0
              THEN RepUR ``csm-ap-type csm-ap cc-fst`` -7
              THEN Auto))
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  L:(Cname  List)  {}\mrightarrow{}  Type
2.  G1  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J)
3.  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
            ((G1  I  K  (f  o  g))  =  ((G1  J  K  g)  o  (G1  I  J  f))))
\mwedge{}  (\mforall{}I:Cname  List.  ((G1  I  I  1)  =  (\mlambda{}x.x)))
4.  A1  :  I:(Cname  List)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  Type
5.  A2  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:(X  I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a))
6.  (\mforall{}I:Cname  List.  \mforall{}a:X  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:X  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))))
7.  u  :  I:(Cname  List)  {}\mrightarrow{}  a:(alpha:X  I  \mtimes{}  (A1  I  alpha))  {}\mrightarrow{}  ((fst((<A1,  A2>)p))  I  a)
8.  <X,  G1>  \mmember{}  CubicalSet
\mvdash{}  istype(\mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:alpha:X  I  \mtimes{}  (A1  I  alpha).
                      ((A2  I  J  f  (fst(a))  (u  I  a))  =  (u  J  f(a))))


By

---

Latex:
(RepeatFor  4  (MemCD')
  THEN  Try  ((Fold  `member`  0
                        THEN  D  -1
                        THEN  RepUR  ``cube-set-restriction``  0
                        THEN  RepUR  ``csm-ap-type  csm-ap  cc-fst``  -7
                        THEN  Auto))
  THEN  Auto)

---

Home Index