---

Step * 2 of Lemma cubical-lambda_wf

.....set predicate..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : {X.A ⊢ _:B}
⊢ ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).
    let A@0,F = ΠA B 
    in (F I J f a ((λb) I a)) = ((λb) J f(a)) ∈ (A@0 J f(a))
BY
{ (RepUR ``cubical-pi cubical-lambda`` 0 THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : {X.A ⊢ _:B}
5. I : Cname List
6. J : Cname List
7. f : name-morph(I;J)
8. a : X(I)
⊢ (λK,g,u. (b K ((f o g)(a);u)))
= (λJ@0,f@0,u. (b J@0 (f@0(f(a));u)))
∈ (J@0:(Cname List) ⟶ f@0:name-morph(J;J@0) ⟶ u:A(f@0(f(a))) ⟶ B((f@0(f(a));u)))

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. b : {X.A ⊢ _:B}
5. I : Cname List
6. J : Cname List
7. f : name-morph(I;J)
8. a : X(I)
9. J@0 : Cname List
10. K : Cname List
11. f@0 : name-morph(J;J@0)
12. g : name-morph(J@0;K)
13. u : A(f@0(f(a)))
⊢ (b J@0 ((f o f@0)(a);u) (f@0(f(a));u) g) = (b K ((f o (f@0 o g))(a);(u f@0(f(a)) g))) ∈ B(g((f@0(f(a));u)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
4.  b  :  \{X.A  \mvdash{}  \_:B\}
\mvdash{}  \mforall{}I,J:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}a:X(I).
        let  A@0,F  =  \mPi{}A  B 
        in  (F  I  J  f  a  ((\mlambda{}b)  I  a))  =  ((\mlambda{}b)  J  f(a))


By

---

Latex:
(RepUR  ``cubical-pi  cubical-lambda``  0  THEN  Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index