---

Step * of Lemma cubical-isect-family-comp

∀X,Delta:⊢. ∀s:Delta ⟶ X. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.
∀w:cubical-isect-family(X;A;B;I;(s)a).
  (λK,g. (w K f ⋅ g) ∈ cubical-isect-family(X;A;B;J;(s)f(a)))
BY
{ ((UnivCD THENA Auto) THEN D -1 THEN MemTypeCD THEN Reduce 0) }

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

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

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

---

Latex:

---

Latex:
\mforall{}X,Delta:\mvdash{}.  \mforall{}s:Delta  {}\mrightarrow{}  X.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:Delta(I).  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.
\mforall{}w:cubical-isect-family(X;A;B;I;(s)a).
    (\mlambda{}K,g.  (w  K  f  \mcdot{}  g)  \mmember{}  cubical-isect-family(X;A;B;J;(s)f(a)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index