---

Step * 1 of Lemma cubical-subset_wf


1. [X] : CubicalSet{j}
2. [T] : {X ⊢ _}
3. [psi] : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. [%] : ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀t:T(a).  (psi[I;a;t] ⇒ psi[J;f(a);(t a f)])
⊢ X ⊢ {t:T | ∀I,alpha. psi[I;alpha;t]}
BY
{ (Unfold `cubical-subset` 0 THEN MemTypeCD) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. psi : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀t:T(a).  (psi[I;a;t] ⇒ psi[J;f(a);(t a f)])
⊢ <λI,alpha. {t:T(alpha)| psi[I;alpha;t]} , λI,J,f,alpha,p. (p alpha f)> ∈ A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ)
                                                                                 ⟶ J:fset(ℕ)
                                                                                 ⟶ f:J ⟶ I
                                                                                 ⟶ a:X(I)
                                                                                 ⟶ (A I a)
                                                                                 ⟶ (A J f(a)))

2
.....set predicate..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. psi : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀t:T(a).  (psi[I;a;t] ⇒ psi[J;f(a);(t a f)])
⊢ let A,F = <λI,alpha. {t:T(alpha)| psi[I;alpha;t]} , λI,J,f,alpha,p. (p alpha f)> 
  in (∀I:fset(ℕ). ∀a:X(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
     ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:A I a.
          ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))

3
.....wf..... 
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. psi : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀t:T(a).  (psi[I;a;t] ⇒ psi[J;f(a);(t a f)])
5. AF : A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a)))
⊢ istype(let A,F = AF 
         in (∀I:fset(ℕ). ∀a:X(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
            ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:X(I). ∀u:A I a.
                 ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a)))))

---

Latex:

---

Latex:

1.  [X]  :  CubicalSet\{j\}
2.  [T]  :  \{X  \mvdash{}  \_\}
3.  [psi]  :  I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  \mBbbP{}
4.  [\%]  :  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:X(I).  \mforall{}t:T(a).    (psi[I;a;t]  {}\mRightarrow{}  psi[J;f(a);(t  a  f)])
\mvdash{}  X  \mvdash{}  \{t:T  |  \mforall{}I,alpha.  psi[I;alpha;t]\}


By

---

Latex:
(Unfold  `cubical-subset`  0  THEN  MemTypeCD)

---

Home Index