---

Step * 1 of Lemma cubical-isect_wf


1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
⊢ <λI,a. cubical-isect-family(X;A;B;I;a), λI,J,f,a,w,K,g. (w K f ⋅ g)> ∈ 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 THEN Reduce 0 THEN Auto THEN D -1 THEN MemTypeCD THEN Reduce 0) }

1
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. J : fset(ℕ)
6. f : J ⟶ I
7. a : X(I)
8. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
9. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(a)).  ((w J f (f(a);u) g) = (w K f ⋅ g) ∈ B(g((f(a);u))))
⊢ λK,g. (w K f ⋅ g) ∈ J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ (⋂u:A(f@0(f(a))). B((f@0(f(a));u)))

2
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. J : fset(ℕ)
6. f : J ⟶ I
7. a : X(I)
8. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
9. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(a)).  ((w J f (f(a);u) g) = (w K f ⋅ g) ∈ B(g((f(a);u))))
⊢ ∀J@0,K:fset(ℕ). ∀f@0:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:A(f@0(f(a))).
    ((w J@0 f ⋅ f@0 (f@0(f(a));u) g) = (w K f ⋅ f@0 ⋅ g) ∈ B(g((f@0(f(a));u))))

3
.....wf..... 
1. X : CubicalSet
2. A : {X ⊢ _}
3. B : {X.A ⊢ _}
4. I : fset(ℕ)
5. J : fset(ℕ)
6. f : J ⟶ I
7. a : X(I)
8. w : J:fset(ℕ) ⟶ f:J ⟶ I ⟶ (⋂u:A(f(a)). B((f(a);u)))
9. ∀J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀u:A(f(a)).  ((w J f (f(a);u) g) = (w K f ⋅ g) ∈ B(g((f(a);u))))
10. w1 : J@0:fset(ℕ) ⟶ f@0:J@0 ⟶ J ⟶ (⋂u:A(f@0(f(a))). B((f@0(f(a));u)))
⊢ istype(∀J@0,K:fset(ℕ). ∀f@0:J@0 ⟶ J. ∀g:K ⟶ J@0. ∀u:A(f@0(f(a))).
           ((w1 J@0 f@0 (f@0(f(a));u) g) = (w1 K f@0 ⋅ g) ∈ B(g((f@0(f(a));u)))))

---

Latex:

---

Latex:

1.  X  :  CubicalSet
2.  A  :  \{X  \mvdash{}  \_\}
3.  B  :  \{X.A  \mvdash{}  \_\}
\mvdash{}  <\mlambda{}I,a.  cubical-isect-family(X;A;B;I;a),  \mlambda{}I,J,f,a,w,K,g.  (w  K  f  \mcdot{}  g)>  \mmember{}  A:I:fset(\mBbbN{})  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type\000C  \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  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index