---

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


1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
4. sigma : A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (Delta A) (Gamma A))
5. ∀A,B:cat-ob(NameCat). ∀g:cat-arrow(NameCat) A B.
     ((cat-comp(TypeCat) (Delta A) (Gamma A) (Gamma B) (sigma A) (Gamma A B g))
     = (cat-comp(TypeCat) (Delta A) (Delta B) (Gamma B) (Delta A B g) (sigma B))
     ∈ (cat-arrow(TypeCat) (Delta A) (Gamma B)))
6. u : {Delta ⊢ _:(A)sigma}
7. x : cat-ob(NameCat)
⊢ (sigma x) = (λx@0.(sigma x x@0)) ∈ (((fst(Delta)) x) ⟶ ((fst(Gamma)) x))
BY
{ TACTIC:(RepeatFor 2 (DVar `Delta') THEN All Reduce THEN Ext) }

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

2
.....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

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  Delta  :  CubicalSet
3.  A  :  \{Gamma  \mvdash{}  \_\}
4.  sigma  :  A:cat-ob(NameCat)  {}\mrightarrow{}  (cat-arrow(TypeCat)  (Delta  A)  (Gamma  A))
5.  \mforall{}A,B:cat-ob(NameCat).  \mforall{}g:cat-arrow(NameCat)  A  B.
          ((cat-comp(TypeCat)  (Delta  A)  (Gamma  A)  (Gamma  B)  (sigma  A)  (Gamma  A  B  g))
          =  (cat-comp(TypeCat)  (Delta  A)  (Delta  B)  (Gamma  B)  (Delta  A  B  g)  (sigma  B)))
6.  u  :  \{Delta  \mvdash{}  \_:(A)sigma\}
7.  x  :  cat-ob(NameCat)
\mvdash{}  (sigma  x)  =  (\mlambda{}x@0.(sigma  x  x@0))


By

---

Latex:
TACTIC:(RepeatFor  2  (DVar  `Delta')  THEN  All  Reduce  THEN  Ext)

---

Home Index