---

Step * 1 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. 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)))
BY
{ xxx((Assert s1 ∈ I:(Cname List) ⟶ Z(I) ⟶ Delta(I) BY
             Auto)
      THEN (Assert s2 ∈ I:(Cname List) ⟶ Delta(I) ⟶ Gamma(I) BY
                  Auto)
      THEN MemCD
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  Z  :  CubicalSet
4.  s1  :  Z  {}\mrightarrow{}  Delta
5.  s2  :  Delta  {}\mrightarrow{}  Gamma
6.  A1  :  I:(Cname  List)  {}\mrightarrow{}  Gamma(I)  {}\mrightarrow{}  Type
7.  A2  :  I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  f:name-morph(I;J)
{}\mrightarrow{}  a:Gamma(I)
{}\mrightarrow{}  (A1  I  a)
{}\mrightarrow{}  (A1  J  f(a))
8.  let  A,F  =  <A1,  A2> 
      in  (\mforall{}I:Cname  List.  \mforall{}a:Gamma(I).  \mforall{}u:A  I  a.    ((F  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:Gamma(I).  \mforall{}u:A  I  a.
                      ((F  I  K  (f  o  g)  a  u)  =  (F  J  K  g  f(a)  (F  I  J  f  a  u))))
\mvdash{}  <\mlambda{}I,a.  (A1  I  (s2  I  (s1  I  a))),  \mlambda{}I,J,f,a,u.  (A2  I  J  f  (s2  I  (s1  I  a))  u)>  \mmember{}  A:I:(Cname  List)  {}\mrightarrow{}  Z(I\000C)  {}\mrightarrow{}  Type
    \mtimes{}  (I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  f:name-morph(I;J)  {}\mrightarrow{}  a:Z(I)  {}\mrightarrow{}  (A  I  a)  {}\mrightarrow{}  (A  J  f(a)))


By

---

Latex:
xxx((Assert  s1  \mmember{}  I:(Cname  List)  {}\mrightarrow{}  Z(I)  {}\mrightarrow{}  Delta(I)  BY
                      Auto)
        THEN  (Assert  s2  \mmember{}  I:(Cname  List)  {}\mrightarrow{}  Delta(I)  {}\mrightarrow{}  Gamma(I)  BY
                                Auto)
        THEN  MemCD
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index