---

Step * 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) = (p o (sigma;u) x) ∈ (cat-arrow(TypeCat) (Delta x) (Gamma x))
BY
{ TACTIC:RepUR ``csm-comp cat-arrow functor-ob csm-adjoin trans-comp cat-comp type-cat compose cc-fst csm-ap`` 0 }

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) = (λx@0.(sigma x x@0)) ∈ (((fst(Delta)) x) ⟶ ((fst(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\}
7.  x  :  cat-ob(NameCat)
\mvdash{}  (sigma  x)  =  (p  o  (sigma;u)  x)


By

---

Latex:
TACTIC:...

---

Home Index