---

Step * 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}
⊢ sigma = p o (sigma;u) ∈ (A:cat-ob(NameCat) ⟶ (cat-arrow(TypeCat) (Delta A) (Gamma A)))
BY
{ TACTIC:(Ext THENA Auto) }

1
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) = (p o (sigma;u) x) ∈ (cat-arrow(TypeCat) (Delta x) (Gamma x))

---

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\}
\mvdash{}  sigma  =  p  o  (sigma;u)


By

---

Latex:
TACTIC:(Ext  THENA  Auto)

---

Home Index