---

Step * 1 of Lemma cubical-beta

.....assertion..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : {X.A ⊢ _:B}
5. u : {X ⊢ _:A}
⊢ (b)[u] = app((λb); u) ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst((B)[u])) I a))
BY
{ (RepeatFor 2 ((Ext THENA Auto))
   THEN RenameVar `I' (-2)
   THEN RenameVar `a' (-1)
   THEN RepUR ``cubical-app cubical-lambda cubical-pi cc-fst cc-snd csm-ap-term csm-ap`` 0
   THEN (OnVar `b' (\h. D h THEN Fold `cubical-type-at` h)⋅ THEN OnVar `u' (\h. D h THEN Fold `cubical-type-at` h)⋅)
   THEN Fold `cubical-type-at` 0
   THEN RepUR ``csm-id-adjoin csm-adjoin csm-id csm-ap identity-trans cat-id type-cat`` 0
   THEN Fold `cc-adjoin-cube` 0
   THEN (GenConclTerm ⌜u I a⌝⋅ THENA Auto)) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : I:(Cname List) ⟶ a:X.A(I) ⟶ B(a)
5. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X.A(I).  let A@0,F = B in (F I J f a (b I a)) = (b J f(a)) ∈ (A@0 J f(a))
6. u : I:(Cname List) ⟶ a:X(I) ⟶ A(a)
7. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = A in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))
8. I : Cname List
9. a : X(I)
10. v : A(a)
11. (u I a) = v ∈ A(a)
⊢ (b I (a;v)) = (b I (1(a);v)) ∈ (B)λI,a. (a;u I a)(a)

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  b  :  \{X.A  \mvdash{}  \_:B\}
5.  u  :  \{X  \mvdash{}  \_:A\}
\mvdash{}  (b)[u]  =  app((\mlambda{}b);  u)


By

---

Latex:
(RepeatFor  2  ((Ext  THENA  Auto))
  THEN  RenameVar  `I'  (-2)
  THEN  RenameVar  `a'  (-1)
  THEN  RepUR  ``cubical-app  cubical-lambda  cubical-pi  cc-fst  cc-snd  csm-ap-term  csm-ap``  0
  THEN  (OnVar  `b'  (\mbackslash{}h.  D  h  THEN  Fold  `cubical-type-at`  h)\mcdot{}
              THEN  OnVar  `u'  (\mbackslash{}h.  D  h  THEN  Fold  `cubical-type-at`  h)\mcdot{}
              )
  THEN  Fold  `cubical-type-at`  0
  THEN  RepUR  ``csm-id-adjoin  csm-adjoin  csm-id  csm-ap  identity-trans  cat-id  type-cat``  0
  THEN  Fold  `cc-adjoin-cube`  0
  THEN  (GenConclTerm  \mkleeneopen{}u  I  a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index