---

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


1. Gamma : CubicalSet
2. A : A:I:(Cname List) ⟶ Gamma(I) ⟶ Type × (I:(Cname List)
                                              ⟶ J:(Cname List)
                                              ⟶ f:name-morph(I;J)
                                              ⟶ a:Gamma(I)
                                              ⟶ (A I a)
                                              ⟶ (A J f(a)))
3. let A,F = A 
   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))))
⊢ A
= (A)1(Gamma)
∈ (A:I:(Cname List) ⟶ Gamma(I) ⟶ Type × (I:(Cname List)
                                          ⟶ J:(Cname List)
                                          ⟶ f:name-morph(I;J)
                                          ⟶ a:Gamma(I)
                                          ⟶ (A I a)
                                          ⟶ (A J f(a))))
BY
{ (D 2
   THEN (Assert Gamma ∈ CubicalSet BY
               Trivial)
   THEN RepeatFor 2 (D 1)
   THEN All Reduce
   THEN RepUR ``csm-ap-type csm-id csm-ap identity-trans cat-id type-cat`` 0
   THEN RepUR ``cubical-type`` 0
   THEN All (RepUR ``I-cube functor-ob``)
   THEN EqCD
   THEN Auto
   THEN RepeatFor 2 ((Ext THEN Reduce 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  A  :  A:I:(Cname  List)  {}\mrightarrow{}  Gamma(I)  {}\mrightarrow{}  Type  \mtimes{}  (I:(Cname  List)
                                                                                            {}\mrightarrow{}  J:(Cname  List)
                                                                                            {}\mrightarrow{}  f:name-morph(I;J)
                                                                                            {}\mrightarrow{}  a:Gamma(I)
                                                                                            {}\mrightarrow{}  (A  I  a)
                                                                                            {}\mrightarrow{}  (A  J  f(a)))
3.  let  A,F  =  A 
      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{}  A  =  (A)1(Gamma)


By

---

Latex:
(D  2
  THEN  (Assert  Gamma  \mmember{}  CubicalSet  BY
                          Trivial)
  THEN  RepeatFor  2  (D  1)
  THEN  All  Reduce
  THEN  RepUR  ``csm-ap-type  csm-id  csm-ap  identity-trans  cat-id  type-cat``  0
  THEN  RepUR  ``cubical-type``  0
  THEN  All  (RepUR  ``I-cube  functor-ob``)
  THEN  EqCD
  THEN  Auto
  THEN  RepeatFor  2  ((Ext  THEN  Reduce  0  THEN  Auto)))

---

Home Index