---

Step * 2 of Lemma universe-comp-op_wf

.....set predicate..... 
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
⊢ composition-uniformity(X;decode(t);compOp(t))
BY
{ ((D 0 THENA Auto) THEN RepUR ``universe-comp-op`` 0 THEN Intros) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. j : {j:ℕ| ¬j ∈ J} 
7. g : J ⟶ I
8. rho : X(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(decode(t))<rho> o iota}
11. a0 : cubical-path-0(X;decode(t);I;i;rho;phi;u)
⊢ ((snd(t(rho))) I i 1 phi u a0 (i1)(rho) g)
= ((snd(t(g,i=j(rho)))) J j 1 g(phi) (u)subset-trans(I+i;J+j;g,i=j;s(phi)) (a0 (i0)(rho) g))
∈ decode(t)(g((i1)(rho)))

2
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. i : {i:ℕ| ¬i ∈ I} 
6. j : {j:ℕ| ¬j ∈ J} 
7. g : J ⟶ I
8. rho : X(I+i)
9. phi : 𝔽(I)
10. u : {I+i,s(phi) ⊢ _:(decode(t))<rho> o iota}
⊢ istype(cubical-path-0(X;decode(t);I;i;rho;phi;u))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
\mvdash{}  composition-uniformity(X;decode(t);compOp(t))


By

---

Latex:
((D  0  THENA  Auto)  THEN  RepUR  ``universe-comp-op``  0  THEN  Intros)

---

Home Index