---

Step * 2 of Lemma universe-encode_wf


1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : G(I)
⊢ (<(T)<a>, (cT)<a>> a f) = <(T)<f(a)>, (cT)<f(a)>> ∈ (A:{formal-cube(J) ⊢ _} × formal-cube(J) ⊢ CompOp(A))
BY
{ (RepUR ``cubical-universe closed-cubical-universe closed-type-to-type csm-fibrant-type`` 0 THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : G(I)
⊢ ((T)<a>)<f> = (T)<f(a)> ∈ {formal-cube(J) ⊢ _}

2
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. T : {G ⊢ _}
3. cT : G ⊢ CompOp(T)
4. G ⊢' c𝕌
5. I : fset(ℕ)
6. J : fset(ℕ)
7. f : J ⟶ I
8. a : G(I)
⊢ ((cT)<a>)<f> = (cT)<f(a)> ∈ formal-cube(J) ⊢ CompOp(((T)<a>)<f>)

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  T  :  \{G  \mvdash{}  \_\}
3.  cT  :  G  \mvdash{}  CompOp(T)
4.  G  \mvdash{}'  c\mBbbU{}
5.  I  :  fset(\mBbbN{})
6.  J  :  fset(\mBbbN{})
7.  f  :  J  {}\mrightarrow{}  I
8.  a  :  G(I)
\mvdash{}  (<(T)<a>,  (cT)<a>>  a  f)  =  <(T)<f(a)>,  (cT)<f(a)>>


By

---

Latex:
(RepUR  ``cubical-universe  closed-cubical-universe  closed-type-to-type  csm-fibrant-type``  0
  THEN  EqCDA
  )

---

Home Index