---

Step * 1 of Lemma cube-context-adjoin_wf


1. Gamma : CubicalSet
2. A : {Gamma ⊢ _}
3. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((λp.<(f o g)(fst(p)), (snd(p) fst(p) (f o g))>)
     = ((λp.<g(fst(p)), (snd(p) fst(p) g)>) o (λp.<f(fst(p)), (snd(p) fst(p) f)>))
     ∈ ((alpha:Gamma(I) × A(alpha)) ⟶ (alpha:Gamma(K) × A(alpha))))
4. I : Cname List
⊢ (λp.<1(fst(p)), (snd(p) fst(p) 1)>) = (λx.x) ∈ ((alpha:Gamma(I) × A(alpha)) ⟶ (alpha:Gamma(I) × A(alpha)))
BY
{ ((EqCD THENA Auto) THEN D -1 THEN Reduce 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
          ((\mlambda{}p.<(f  o  g)(fst(p)),  (snd(p)  fst(p)  (f  o  g))>)
          =  ((\mlambda{}p.<g(fst(p)),  (snd(p)  fst(p)  g)>)  o  (\mlambda{}p.<f(fst(p)),  (snd(p)  fst(p)  f)>)))
4.  I  :  Cname  List
\mvdash{}  (\mlambda{}p.ə(fst(p)),  (snd(p)  fst(p)  1)>)  =  (\mlambda{}x.x)


By

---

Latex:
((EqCD  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  EqCD  THEN  Auto)

---

Home Index