---

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


1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
⊢ 1(Gamma.A) = (p;q) ∈ (I:(Cname List) ⟶ Gamma.A(I) ⟶ Gamma.A(I))
BY
{ (RepeatFor 2 (DVar `A')
   THEN (RepUR ``csm-adjoin cc-fst cc-snd I-cube cube-context-adjoin csm-ap csm-id functor-ob`` 0
         THEN RepUR ``identity-trans cat-id type-cat`` 0
         )
   THEN (Fold `functor-ob` 0 THEN Fold `I-cube` 0)
   THEN Auto
   THEN RepeatFor 2 ((Ext THENA Auto))
   THEN Reduce 0) }

1
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))

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  A  :  \{Gamma  \mvdash{}  \_\}
\mvdash{}  1(Gamma.A)  =  (p;q)


By

---

Latex:
(RepeatFor  2  (DVar  `A')
  THEN  (RepUR  ``csm-adjoin  cc-fst  cc-snd  I-cube  cube-context-adjoin  csm-ap  csm-id  functor-ob``  0
              THEN  RepUR  ``identity-trans  cat-id  type-cat``  0
              )
  THEN  (Fold  `functor-ob`  0  THEN  Fold  `I-cube`  0)
  THEN  Auto
  THEN  RepeatFor  2  ((Ext  THENA  Auto))
  THEN  Reduce  0)

---

Home Index