---

Step * 1 of Lemma csm-ap-comp-type


1. Gamma : CubicalSet
2. Delta : CubicalSet
3. Z : CubicalSet
4. s1 : Z ⟶ Delta
5. s2 : Delta ⟶ Gamma
6. A : {Gamma ⊢ _}
⊢ (A)s2 o s1
= ((A)s2)s1
∈ (A:I:(Cname List) ⟶ Z(I) ⟶ Type × (I:(Cname List)
                                      ⟶ J:(Cname List)
                                      ⟶ f:name-morph(I;J)
                                      ⟶ a:Z(I)
                                      ⟶ (A I a)
                                      ⟶ (A J f(a))))
BY
{ xxx(RepeatFor 2 (DVar `A')
      THEN RepUR ``csm-ap-type csm-ap csm-comp trans-comp cat-comp type-cat compose`` 0
      THEN Fold `member` 0)xxx }

1
1. Gamma : CubicalSet
2. Delta : CubicalSet
3. Z : CubicalSet
4. s1 : Z ⟶ Delta
5. s2 : Delta ⟶ Gamma
6. A1 : I:(Cname List) ⟶ Gamma(I) ⟶ Type
7. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:Gamma(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
8. let A,F = <A1, A2> 
   in (∀I:Cname List. ∀a:Gamma(I). ∀u:A I a.  ((F 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:Gamma(I). ∀u:A I a.
           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))
⊢ <λI,a. (A1 I (s2 I (s1 I a))), λI,J,f,a,u. (A2 I J f (s2 I (s1 I a)) u)> ∈ A:I:(Cname List) ⟶ Z(I) ⟶ Type × (I:(Cnam\000Ce List)
                                                                                                  ⟶ J:(Cname List)
                                                                                                  ⟶ f:name-morph(I;J)
                                                                                                  ⟶ a:Z(I)
                                                                                                  ⟶ (A I a)
                                                                                                  ⟶ (A J f(a)))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  Z  :  CubicalSet
4.  s1  :  Z  {}\mrightarrow{}  Delta
5.  s2  :  Delta  {}\mrightarrow{}  Gamma
6.  A  :  \{Gamma  \mvdash{}  \_\}
\mvdash{}  (A)s2  o  s1  =  ((A)s2)s1


By

---

Latex:
xxx(RepeatFor  2  (DVar  `A')
        THEN  RepUR  ``csm-ap-type  csm-ap  csm-comp  trans-comp  cat-comp  type-cat  compose``  0
        THEN  Fold  `member`  0)xxx

---

Home Index