---

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


1. Gamma : CubicalSet
2. X : L:(Cname List) ⟶ Type
3. D1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
4. (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
      ((D1 I K (f o g)) = ((D1 J K g) o (D1 I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((D1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))
5. A : {Gamma ⊢ _}
6. sigma : A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (<X, D1> A) (Gamma A))
7. ∀A,B:cat-ob(NameCat). ∀g:cat-arrow(NameCat) A B.
     ((cat-comp(TypeCat) (<X, D1> A) (Gamma A) (Gamma B) (sigma A) (Gamma A B g))
     = (cat-comp(TypeCat) (<X, D1> A) (<X, D1> B) (Gamma B) (<X, D1> A B g) (sigma B))
     ∈ (cat-arrow(TypeCat) (<X, D1> A) (Gamma B)))
8. u : {<X, D1> ⊢ _:(A)sigma}
9. x : cat-ob(NameCat)
10. x1 : X x
⊢ (sigma x x1) = ((λx@0.(sigma x x@0)) x1) ∈ ((fst(Gamma)) x)
BY
{ TACTIC:(RepUR ``cat-arrow type-cat functor-ob`` -5 THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  X  :  L:(Cname  List)  {}\mrightarrow{}  Type
3.  D1  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J)
4.  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
            ((D1  I  K  (f  o  g))  =  ((D1  J  K  g)  o  (D1  I  J  f))))
\mwedge{}  (\mforall{}I:Cname  List.  ((D1  I  I  1)  =  (\mlambda{}x.x)))
5.  A  :  \{Gamma  \mvdash{}  \_\}
6.  sigma  :  A:cat-ob(NameCat)  {}\mrightarrow{}  (cat-arrow(TypeCat)  (<X,  D1>  A)  (Gamma  A))
7.  \mforall{}A,B:cat-ob(NameCat).  \mforall{}g:cat-arrow(NameCat)  A  B.
          ((cat-comp(TypeCat)  (<X,  D1>  A)  (Gamma  A)  (Gamma  B)  (sigma  A)  (Gamma  A  B  g))
          =  (cat-comp(TypeCat)  (<X,  D1>  A)  (<X,  D1>  B)  (Gamma  B)  (<X,  D1>  A  B  g)  (sigma  B)))
8.  u  :  \{<X,  D1>  \mvdash{}  \_:(A)sigma\}
9.  x  :  cat-ob(NameCat)
10.  x1  :  X  x
\mvdash{}  (sigma  x  x1)  =  ((\mlambda{}x@0.(sigma  x  x@0))  x1)


By

---

Latex:
TACTIC:(RepUR  ``cat-arrow  type-cat  functor-ob``  -5  THEN  Auto)

---

Home Index