---

Step * 1 of Lemma cubical-eta

.....assertion..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. w : {X ⊢ _:ΠA B}
⊢ w = (λapp((w)p; q)) ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst(ΠA B)) I a))
BY
{ xxx(RepeatFor 2 ((Ext THENA Auto))
      THEN RepUR ``cubical-app cubical-lambda cubical-pi cc-fst cc-snd csm-ap-term csm-ap`` 0
      THEN OnVar `w' (\h. D h THEN RepUR ``cubical-pi`` h)
      THEN RenameVar `I' (-2)
      THEN RenameVar `a' (-1))xxx }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. w : I:(Cname List) ⟶ a:X(I) ⟶ cubical-pi-family(X;A;B;I;a)
5. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = ΠA B in (F I J f a (w I a)) = (w J f(a)) ∈ (A J f(a))
6. I : Cname List
7. a : X(I)
⊢ (w I a) = (λJ,f,u. (w J (fst((f(a);u))) J 1 (snd((f(a);u))))) ∈ cubical-pi-family(X;A;B;I;a)

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  w  :  \{X  \mvdash{}  \_:\mPi{}A  B\}
\mvdash{}  w  =  (\mlambda{}app((w)p;  q))


By

---

Latex:
xxx(RepeatFor  2  ((Ext  THENA  Auto))
        THEN  RepUR  ``cubical-app  cubical-lambda  cubical-pi  cc-fst  cc-snd  csm-ap-term  csm-ap``  0
        THEN  OnVar  `w'  (\mbackslash{}h.  D  h  THEN  RepUR  ``cubical-pi``  h)
        THEN  RenameVar  `I'  (-2)
        THEN  RenameVar  `a'  (-1))xxx

---

Home Index