---

Step * 1 1 of Lemma csm-adjoin-fst-snd


1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A1 : I:(Cname List) ⟶ Gamma(I) ⟶ Type
4. A2 : I:(Cname List) ⟶ J:(Cname List) ⟶ f:name-morph(I;J) ⟶ a:Gamma(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. 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))))
6. x : Cname List
7. x1 : alpha:Gamma(x) × <A1, A2>(alpha)
⊢ x1 = <ob(x1), snd(x1)> ∈ (alpha:Gamma(x) × <A1, A2>(alpha))
BY
{ ((D -1 THEN RepUR ``functor-ob`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  A1  :  I:(Cname  List)  {}\mrightarrow{}  Gamma(I)  {}\mrightarrow{}  Type
4.  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))
5.  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))))
6.  x  :  Cname  List
7.  x1  :  alpha:Gamma(x)  \mtimes{}  <A1,  A2>(alpha)
\mvdash{}  x1  =  <ob(x1),  snd(x1)>


By

---

Latex:
((D  -1  THEN  RepUR  ``functor-ob``  0)  THEN  Auto)

---

Home Index