---

Step * 2 of Lemma universe-decode_wf


1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌')
4. ∀[u:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ c𝕌(a))
⊢ (∀I:fset(ℕ). ∀a:X(I). ∀u:fst(t(a))(1).  ((u 1 1) = u ∈ fst(t(a))(1)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:fst(t(a))(1).  ((u 1 f ⋅ g) = ((u 1 f) 1 g) ∈ fst(t(f ⋅ g(a)))(1)))
BY
{ (D 0 THEN RepeatFor 2 (Intro)) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌')
4. ∀[u:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ c𝕌(a))
5. I : fset(ℕ)
6. a : X(I)
⊢ ∀u:fst(t(a))(1). ((u 1 1) = u ∈ fst(t(a))(1))

2
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. ∀I:fset(ℕ). ∀a:Top.  (c𝕌(a) ∈ 𝕌')
4. ∀[u:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)].  (u(a) ∈ c𝕌(a))
5. I : fset(ℕ)
6. J : fset(ℕ)
⊢ ∀K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:fst(t(a))(1).  ((u 1 f ⋅ g) = ((u 1 f) 1 g) ∈ fst(t(f ⋅ g(a)))(1))

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  t  :  \{X  \mvdash{}  \_:c\mBbbU{}\}
3.  \mforall{}I:fset(\mBbbN{}).  \mforall{}a:Top.    (c\mBbbU{}(a)  \mmember{}  \mBbbU{}')
4.  \mforall{}[u:\{X  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[a:X(I)].    (u(a)  \mmember{}  c\mBbbU{}(a))
\mvdash{}  (\mforall{}I:fset(\mBbbN{}).  \mforall{}a:X(I).  \mforall{}u:fst(t(a))(1).    ((u  1  1)  =  u))
\mwedge{}  (\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:X(I).  \mforall{}u:fst(t(a))(1).    ((u  1  f  \mcdot{}  g)  =  ((u  1  f)  1  g)))


By

---

Latex:
(D  0  THEN  RepeatFor  2  (Intro))

---

Home Index