---

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

.....wf..... 
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)
⊢ (X x) = (X x) ∈ Type
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:
.....wf..... 
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)
\mvdash{}  (X  x)  =  (X  x)


By

---

Latex:
TACTIC:Auto

---

Home Index