---

Step * 1 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,a. fst(t(a))(1), λI,J,f,a,x. (x 1 f)> ∈ A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ)
                                                              ⟶ J:fset(ℕ)
                                                              ⟶ f:J ⟶ I
                                                              ⟶ a:X(I)
                                                              ⟶ (A I a)
                                                              ⟶ (A J f(a)))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
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,a. fst(t(a))(1) ∈ I:fset(ℕ) ⟶ X(I) ⟶ Type

2
.....subterm..... T:t
2:n
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,J,f,a,x. (x 1 f) ∈ I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ ((λI,a. fst(t(a))(1)) I a) ⟶ ((λI,a. fst(t(a))(\000C1)) J f(a))

3
.....eq aux..... 
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. A : I:fset(ℕ) ⟶ X(I) ⟶ Type
⊢ istype(I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a)))

---

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{}  <\mlambda{}I,a.  fst(t(a))(1),  \mlambda{}I,J,f,a,x.  (x  1  f)>  \mmember{}  A:I:fset(\mBbbN{})  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type  \mtimes{}  (I:fset(\mBbbN{})
                                                                                                                            {}\mrightarrow{}  J:fset(\mBbbN{})
                                                                                                                            {}\mrightarrow{}  f:J  {}\mrightarrow{}  I
                                                                                                                            {}\mrightarrow{}  a:X(I)
                                                                                                                            {}\mrightarrow{}  (A  I  a)
                                                                                                                            {}\mrightarrow{}  (A  J  f(a)))


By

---

Latex:
MemCD

---

Home Index